×

zbMATH — the first resource for mathematics

Mu-calculus path checking. (English) Zbl 1184.68339
Summary: We investigate the path model checking problem for the \(\mu \)-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the \(\mu \)-calculus.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
APMC; JPAX
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Artho, C.; Barringer, H.; Goldberg, A.; Havelund, K.; Khurshid, S.; Lowry, M.; Pasareanu, C.; Roşu, G.; Sen, K.; Visser, W.; Washington, R., Combining test case generation and runtime verification, Theoret. comput. sci., 336, 2-3, 209-234, (2005) · Zbl 1080.68062
[2] Bradfield, J.C., The modal mu-calculus alternation hierarchy is strict, Theoret. comput. sci., 195, 2, 133-153, (1998) · Zbl 0915.03017
[3] Bradfield, J.C.; Stirling, C., Modal logics and mu-calculi: an introduction, (), 293-330, (Chapter 4) · Zbl 1002.03021
[4] Demri, S.; Schnoebelen, Ph., The complexity of propositional linear temporal logics in simple cases, Inform. and comput., 174, 1, 84-103, (2002) · Zbl 1009.68072
[5] Havelund, K.; Roşu, G., An overview of the runtime verification tool Java pathexplorer, Formal methods in system design, 24, 2, 189-215, (2004) · Zbl 1073.68549
[6] Hérault, T.; Lassaigne, R.; Magniette, F.; Peyronnet, S., Approximate probabilistic model checking, (), 73-84 · Zbl 1202.68249
[7] Jurdziński, M., Deciding the winner in parity games is in \(\operatorname{UP} \cap \operatorname{coUP}\), Inform. process. lett., 68, 3, 119-124, (1998) · Zbl 1338.68109
[8] Markey, N.; Schnoebelen, Ph., Model checking a path (preliminary report), (), 251-265 · Zbl 1274.68197
[9] Mateescu, R., Local model-checking of modal mu-calculus on acyclic labeled transition systems, (), 281-295 · Zbl 1043.68596
[10] Niwiński, D., On fixed point clones, (), 464-473
[11] Roger, M.; Goubault-Larrecq, J., Log auditing through model checking, (), 220-236
[12] M.Y. Vardi, A temporal fixpoint calculus, in: Proc. 15th ACM Symp. Principles of Programming Languages (POPL’88), San Diego, CA, USA, January 1988, pp. 250-259
[13] Vardi, M.Y., Reasoning about the past with two-way automata, (), 628-641 · Zbl 0909.03019
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.