{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T10:12:48Z","timestamp":1742638368664},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540583295"},{"type":"electronic","value":"9783540486541"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/978-3-540-48654-1_8","type":"book-chapter","created":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T09:34:34Z","timestamp":1462872874000},"page":"81-97","source":"Crossref","is-referenced-by-count":5,"title":["Verification of Nonregular Temporal Properties for Context-Free Processes"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rachid","family":"Echahed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riadh","family":"Robbana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of Bisimulation Equiva-lence for Processes Generating Context-Free Languages. Tech. Rep. CS-R8632, 1987. CWI.","DOI":"10.1007\/3-540-17945-3_5"},{"key":"8_CR2","volume-title":"8th Symp. on Logic in Computer Science. IEEE","author":"A Bouajjani","year":"1993","unstructured":"A. Bouajjani, R. Echahed, and J. Sifakis. On Model Checking for Real-Time Proper-ties with Durations. In 8th Symp. on Logic in Computer Science. IEEE, 1993."},{"key":"8_CR3","volume-title":"Computability and Logic","author":"GS Boolos","year":"1974","unstructured":"G.S. Boolos and R.C. Jeffrey. Computability and Logic. Cambridge Univ. Press, 1974."},{"key":"8_CR4","unstructured":"O. Burkart and B. Steffen. Model Checking for Context-Free Processes. In CONCUR\u201992. Springer-Verlag, 1992. LNCS 630."},{"key":"8_CR5","unstructured":"J.R. Buchi. On a Decision Method in Restricted Second Order Arithmetic. In Intern. Cong. Logic, Method and Philos. Sci. Stanford Univ. Press, 1962."},{"key":"8_CR6","volume-title":"10th ACM Symp. on Principles of Programming Languages. ACM","author":"EM Clarke","year":"1983","unstructured":"E.M. Clarke, E.A. Emerson, and E. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications: A Practical Approach. In 10th ACM Symp. on Principles of Programming Languages. ACM, 1983."},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z Chaochen","year":"1991","unstructured":"Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. Information Processing Letters, 40: 269\u2013276, 1991.","journal-title":"Information Processing Letters"},{"key":"8_CR8","unstructured":"S. Christensen, H. H\u00fcttel, and C. Stirling. Bisimulation Equivalence is Decidable for all Context-Free Processes. In CONCUR\u201992. Springer-Verlag, 1992. LNCS 630."},{"key":"8_CR9","volume-title":"Popl. Acm","author":"EA Emerson","year":"1983","unstructured":"E.A. Emerson and J.Y. Halpern. \u2018Sometimes\u2019 and \u2018Not Never\u2019 Revisited: On Branching versus Linear Time Logic. In POPL. ACM, 1983."},{"key":"8_CR10","volume-title":"First Symp. on Logic in Computer Science","author":"EA Emerson","year":"1986","unstructured":"E.A. Emerson and C.L. Lei. Efficient Model-Checking in Fragments of the Propositional p-Calculus. In First Symp. on Logic in Computer Science, 1986."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Uniform Inevitability is Tree Automaton Ineffable. Information Processing Letters, 24, 1987.","DOI":"10.1016\/0020-0190(87)90097-4"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"M.J. Fischer and R.E. Ladner. Propositional Dynamic Logic of Regular Programs. J. Comp. Syst. Sci., 18, 1979.","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"8_CR13","volume-title":"Undecidable Equivalences for Basic Process Algebra. Tech. Rep","author":"JF Groote","year":"1991","unstructured":"J.F. Groote and H. H\u00fcttel. Undecidable Equivalences for Basic Process Algebra. Tech. Rep. ECS-LFCS-91\u2013169, 1991. Dep. of Computer Science, Univ. of Edinburgh."},{"key":"8_CR14","volume-title":"7th Symp. on Principles of Programming Languages. ACM","author":"D Gabbay","year":"1980","unstructured":"D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the Temporal Analysis of Fairness. In 7th Symp. on Principles of Programming Languages. ACM, 1980."},{"key":"8_CR15","volume-title":"Comp","author":"MA Harrison","year":"1978","unstructured":"M.A. Harrison. Introduction to Formal Language Theory. Addison-Wesley Pub. Comp., 1978."},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"D. Harel and M.S. Paterson. Undecidability of PDL with L = {a2 | i > 0}. J. Comp. Syst. Sci., 29, 1984.","DOI":"10.1016\/0022-0000(84)90005-9"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"D. Harel, A. Pnueli, and J. Stavi. Propositional Dynamic Logic of Nonregular Programs. J. Comp. Syst. Sci., 26, 1983.","DOI":"10.1016\/0022-0000(83)90014-4"},{"key":"8_CR18","volume-title":"31th Symp. on Foundations of Computer Science, pages 652-661. IEEE","author":"D Harel","year":"1990","unstructured":"D. Harel and D. Raz. Deciding Properties of Nonregular Programs. In 31th Symp. on Foundations of Computer Science, pages 652\u2013661. IEEE, 1990."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the Propositional \u03bc-Calculus. Theo. Comp. Sci., 27, 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"T. Koren and A. Pnueli. There Exist Decidable Context-Free Propositional Dynamic Logics. In Proc. Symp. on Logics of Programs. Springer-Verlag, 1983. LNCS 164.","DOI":"10.1007\/3-540-12896-4_369"},{"key":"8_CR21","volume-title":"Lics. Ieee","author":"D Niwinski","year":"1988","unstructured":"D. Niwinski. Fixed Points vs. Infinite Generation. In LICS. IEEE, 1988."},{"key":"8_CR22","volume-title":"Focs. Ieee","author":"A Pnueli","year":"1977","unstructured":"A. Pnueli. The Temporal Logic of Programs. In FOCS. IEEE, 1977."},{"key":"8_CR23","volume-title":"Focs. Ieee","author":"VR Pratt","year":"1981","unstructured":"V.R. Pratt. A Decidable Mu-Calculus: Preliminary Report. In FOCS. IEEE, 1981."},{"key":"8_CR24","first-page":"137","volume-title":"Intern. Symp. on Programming, LNCS","author":"J-P Queille","year":"1982","unstructured":"J-P. Queille and J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. In Intern. Symp. on Programming, LNCS 137, 1982."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"M.O. Rabin. Decidability of Second Order Theories and Automata on Infinite Trees. Trans. Amer. Math. Soc., 141, 1969.","DOI":"10.2307\/1995086"},{"key":"8_CR26","volume-title":"McGraw-Hill Book Comp","author":"H Rogers","year":"1967","unstructured":"H. Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill Book Comp., 1967."},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"R.S. Streett and E.A. Emerson. The Propositional \u03bc-Calculus is Elementary. In ICALP. Springer-Verlag, 1984. LNCS 172.","DOI":"10.1007\/3-540-13345-3_43"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"R.S. Streett. Propositional Dynamic Logic of Looping and Converse is Elementary Decidable. Information and Control, 54, 1982.","DOI":"10.1016\/S0019-9958(82)91258-X"},{"key":"8_CR29","volume-title":"2nd Symp. on Logic in Computer Science","author":"W Thomas","year":"1987","unstructured":"W. Thomas. On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees. In 2nd Symp. on Logic in Computer Science, 1987."},{"key":"8_CR30","volume-title":"Popl. Acm","author":"MY Vardi","year":"1988","unstructured":"M.Y. Vardi. A Temporal Fixpoint Calculus. In POPL. ACM, 1988."},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi and P. Wolper. Automata-Theoretic Techniques for Modal Logics of Programs. J. Comp. Syst. Sci., 32, 1986.","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"P. Wolper. Temporal Logic Can Be More Expressive. Inform. and Control, 56, 1983.","DOI":"10.1016\/S0019-9958(83)80051-5"}],"container-title":["Lecture Notes in Computer Science","CONCUR '94: Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-48654-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T14:50:39Z","timestamp":1558795839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-48654-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540583295","9783540486541"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-48654-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}