Abstract
Decidability of modal logics is not limited to finite systems. The alternation-free modal mu-calculus has already been shown to be decidable for context-free processes, with a worst case complexity which is linear in the size of the system description and exponential in the size of the formula. Like context-free processes correspond to the concept of procedures without parameters, macro processes correspond to procedures with procedure parameters. They too allow deciding mu-calculus formulae, as is shown in this paper by presenting both global (iterative) and local (tableaux-based) procedures. These decision procedures handle correctly also process systems which are defined by unguarded recursion. As expected, the worst case complexity depends on the highest type level in the process description, and it is k-exponential in the size of the formula for a system description with type level k.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andersen, H., Model checking on boolean graphs. ESOP '92, LNCS 582 (1992), 1–19.
Bergstra, J.A., and Klop, J.W., Process theory based on bisimulation semantics. LNCS 354 (eds de Bakker, de Roever, Rozenberg) (1988), 50–122.
Bradfield, J.C., Verifying temporal properties of systems. BirkhÄuser, Boston (1992).
Bradfield, J.C., and Stirling, C. P., Verifying temporal properties of processes. Proc. CONCUR '90, LNCS 458 (1990), 115–125.
Burkart, O., and Steffen, B., Model checking for context-free processes. CONCUR '92, LNCS 630 (1992), 123–137.
Burkart, O., and Steffen, B., Pushdown processes: Parallel composition and model checking. Tech. Rep. Aachen/Passau (1994), 17 p. (1992), 123–137.
Caucal, D., and Monfort, R., On the transition graphs of automata and languages. WG 90, LNCS 484 (1990), 311–337.
Clarke, E.M., Emerson, E.A., and Sistla, A.P., Automatic verification of finite state concurrent systems using temporal logic specifications. ACM TOPLAS 8 (1986), 244–263.
Cleaveland, R., Tableau-based model checking in the propositional mucalculus. Acta Inf. 27 (1990), 725–747.
Cleaveland, R., Parrow, J., and Steffen, B., The concurrency workbench. Workshop Automatic Verification Methods for Finite-State Systems, LNCS 407 (1989), 24–37.
Cleaveland, R., and Steffen, B., Computing behavioral relations, logically. ICALP '91, LNCS 510 (1991).
Cleaveland, R., and Steffen, B., A linear-time model-checking algorithm for the alternation-free modal mu-calculus. CAV 91, LNCS 575 (1992), 48–58.
Damm, W., The IO-and OI-hierarchies, TCS 20 (1982), 95–205.
Damm, W., and Goerdt, A., An automata-theoretic characterization of the OI-hierarchy, Inf. and Cont. 71 (1986), 1–32.
Emerson, E.A., and Lei, C.-L., Efficient model checking in fragments of the propositional mu-calculus. 1st LiCS (1986), 267–278.
Engelfriet, J., and Schmidt, E.M., IO and OI, JCSS 15 (1977), 328–353, and JCSS 16 (1978), 67–99.
Fischer, M.J., Grammars with macro-like productions, 9th Conf. Switching and Automata Theory, IEEE (1968), 131–142.
German, S. M., Clarke, E. M. and Halpern, J. Y., Reasoning about procedures as parameters in the language L4, Inf. and Comp. 83 (1989) 265–359. (Earlier version: 1st LiCS (1986) 11–25)
Goerdt, A., A Hoare calculus for functions defined by recursion on higher types, Logics of Programs 1985, LNCS 193, 106–117.
Habel, A., Hyperedge replacement: Grammars and languages. PhD thesis, Bremen (1989), 193 p.
Habel, A., and Kreowski, H.-J., May we introduce to you: Hyperedge replacement, Graph-grammars and their application to computer science 1986, LNCS 291 (1987), 15–26.
Hungar, H., Complexity of proving program correctness, TACS '91, LNCS 526 (1991), 459–474.
Hungar, H. The complexity of verifying functional programs, STACS '93, LNCS 665 (1993), 428–439.
Hungar, H., and Steffen, B., Local model checking for context-free processes. ICALP '93, LNCS 700 (1993), 593–605.
Huynh, D.T., and Tian, L., Deciding bisimilarity of normed context-free processes is in σ p2 . Tech. Rep. UTDCS-1-92, Univ. Texas Dallas (1992).
Iyer, S.P., A note on model checking context-free processes, North American Process Algebra Workshop '93 (ed. Bard Bloom).
Kowalczyk, W., Niwinski, D., and Tiuryn, J. A generalization of Cook's auxiliarypushdown-automata theorem, Fund. Inf. 12 (1989) 497–506.
Kozen, D., Results on the propositional Μ-calculus. TCS 27 (1983), 333–354.
Kfoury, A. J., Tiuryn, J. and Urzyczyn, P., The hierarchie of finitely typed functions, 2nd LiCS (1987) 225–235.
Larsen, K. G., Proof systems for satisfiability in Hennessy-Milner logic with recursion. TCS 72 (1990), 265–288.
Larsen, K.G., Efficient local correctness checking. CAV '92.
Muller, D.E., and Schupp, P.E., The theory of ends, pushdown automata, and second-order logic. TCS 37 (1985), 51–75.
Stirling, C. P., and Walker, D. J., Local model checking in the modal mu-calculus. TAPSOFT '89, LNCS 351 (1989), 369–383.
Vergauwen, B., and Lewi, J., A linear local model checking algorithm for CTL. CONCUR '93, LNCS 715 (1993), 447–461.
Winskel, G., A note on model checking the modal mu-calculus. ICALP '89, LNCS 372 (1989), 761–772.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hungar, H. (1994). Model checking of macro processes. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_52
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_52
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive