Abstract
We address the problem of the specification and the verification of processes with infinite-state spaces. Many relevant properties for such processes involve constraints on numbers of occurrences of events (truth of propositions). These properties are nonregular and hence, they are not expressible neither in the usual logics of processes nor by finite-state ω-automata. We propose a logic called PCTL that allows the description of such properties. PCTL is a combination of the branching-time temporal logic CTL with Presburger arithmetic. Mainly, we study the decidability of the satisfaction relation between context-free processes and PCTL formulas. We show that this relation is decidable for a large fragment of PCTL. Furthermore, we study the satisfiability problem for PCTL. We show that this problem is highly undecidable (Σ 11 -complete), even for the fragment where the satisfaction relation is decidable, and exhibit a nontrivial fragment where the satisfiability problem is decidable.
Partially supported by the ESPRIT-BRA project REACT.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
G.S. Boolos and R.C. Jeffrey. Computability and Logic. Cambridge Univ. Press, 1974.
O. Burkart and B. Steffen. Model Checking for Context-Free Processes. In CONCUR’92. Springer-Verlag, 1992. LNCS 630.
J.R. Buchi. On a Decision Method in Restricted Second Order Arithmetic. In Intern. Cong. Logic, Method and Philos. Sci. Stanford Univ. Press, 1962.
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.
Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. Information Processing Letters, 40: 269–276, 1991.
S. Christensen, H. Hüttel, and C. Stirling. Bisimulation Equivalence is Decidable for all Context-Free Processes. In CONCUR’92. Springer-Verlag, 1992. LNCS 630.
E.A. Emerson and J.Y. Halpern. ‘Sometimes’ and ‘Not Never’ Revisited: On Branching versus Linear Time Logic. In POPL. ACM, 1983.
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.
E.A. Emerson. Uniform Inevitability is Tree Automaton Ineffable. Information Processing Letters, 24, 1987.
M.J. Fischer and R.E. Ladner. Propositional Dynamic Logic of Regular Programs. J. Comp. Syst. Sci., 18, 1979.
J.F. Groote and H. Hüttel. Undecidable Equivalences for Basic Process Algebra. Tech. Rep. ECS-LFCS-91–169, 1991. Dep. of Computer Science, Univ. of Edinburgh.
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.
M.A. Harrison. Introduction to Formal Language Theory. Addison-Wesley Pub. Comp., 1978.
D. Harel and M.S. Paterson. Undecidability of PDL with L = {a2 | i > 0}. J. Comp. Syst. Sci., 29, 1984.
D. Harel, A. Pnueli, and J. Stavi. Propositional Dynamic Logic of Nonregular Programs. J. Comp. Syst. Sci., 26, 1983.
D. Harel and D. Raz. Deciding Properties of Nonregular Programs. In 31th Symp. on Foundations of Computer Science, pages 652–661. IEEE, 1990.
D. Kozen. Results on the Propositional μ-Calculus. Theo. Comp. Sci., 27, 1983.
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.
D. Niwinski. Fixed Points vs. Infinite Generation. In LICS. IEEE, 1988.
A. Pnueli. The Temporal Logic of Programs. In FOCS. IEEE, 1977.
V.R. Pratt. A Decidable Mu-Calculus: Preliminary Report. In FOCS. IEEE, 1981.
J-P. Queille and J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. In Intern. Symp. on Programming, LNCS 137, 1982.
M.O. Rabin. Decidability of Second Order Theories and Automata on Infinite Trees. Trans. Amer. Math. Soc., 141, 1969.
H. Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill Book Comp., 1967.
R.S. Streett and E.A. Emerson. The Propositional μ-Calculus is Elementary. In ICALP. Springer-Verlag, 1984. LNCS 172.
R.S. Streett. Propositional Dynamic Logic of Looping and Converse is Elementary Decidable. Information and Control, 54, 1982.
W. Thomas. On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees. In 2nd Symp. on Logic in Computer Science, 1987.
M.Y. Vardi. A Temporal Fixpoint Calculus. In POPL. ACM, 1988.
M.Y. Vardi and P. Wolper. Automata-Theoretic Techniques for Modal Logics of Programs. J. Comp. Syst. Sci., 32, 1986.
P. Wolper. Temporal Logic Can Be More Expressive. Inform. and Control, 56, 1983.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouajjani, A., Echahed, R., Robbana, R. (1994). Verification of Nonregular Temporal Properties for Context-Free Processes. In: Jonsson, B., Parrow, J. (eds) CONCUR ’94: Concurrency Theory. CONCUR 1994. Lecture Notes in Computer Science, vol 836. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-48654-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-48654-1_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58329-5
Online ISBN: 978-3-540-48654-1
eBook Packages: Springer Book Archive