×

Model checking and boolean graphs. (English) Zbl 0798.03017

Summary: We describe a method for translating a satisfaction problem of the modal \(\mu\)-calculus into a problem of finding a certain marking of a Boolean graph. By giving algorithms to solve the graph problem, we present a global model checking algorithm for a subset of the modal \(\mu\)-calculus, which has time-complexity \(O(| A| | T|)\), where \(| A|\) is the size of the assertion and \(| T|\) is the size of the model (a labelled transition system). This algorithm is extended to an algorithm for the full modal \(\mu\)-calculus running in time \(O(| A|^{\text{ad}} | S|^{\text{ad}-1} | T|)\), where ad is the alternation depth and \(| S|\) is the number of states in the transition system, improving on earlier presented algorithms. Moreover, a local algorithm is presented for alternation depth one. This algorithm runs in time \(O(| A| | T|\log (| A| | T|))\) and is also an improvement on earlier algorithms.

MSC:

03B45 Modal logic (including the logic of norms)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q25 Analysis of algorithms and problem complexity
68R10 Graph theory (including graph drawing) in computer science
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Aho, A.V.; Hopcroft, J.E.; Ullman, J.D., The design and analysis of computer algorithms, (1974), Addison-Wesley Reading, MA · Zbl 0207.01701
[2] Andersen, H.R., Local computation of alternating fixed-points, ()
[3] Andersen, H.R., Local computation of simultaneous fixed-points, ()
[4] Andersen, H.R., Verification of temporal properties in concurrent systems, (1993), Department of Computer Science, Aarhus Univ Denmark, Ph.D. Thesis, PB-445
[5] Andersen, H.R.; Winskel, G., Compositional checking of satisfaction, Formal methods in system design, 1, 4, (1992), extended abstract in [19] · Zbl 0776.68083
[6] Arnold, A.; Crubille, P., A linear algorithm to solve fixed-point equations on transitions systems, Inform. process. lett., 29, 57-66, (1988) · Zbl 0663.68075
[7] Bekić, H., Definable operations in general algebras, and the theory of automata and flow charts, (), 30-55
[8] Cleaveland, R., Tableau-based model checking in the propositional mu-calculus, Acta inform., 27, 725-747, (1990) · Zbl 0676.03033
[9] Cleaveland, R.; Parrow, J.; Steffen, B., The concurrency workbench: A semantics based tool for the verification of concurrent systems, ()
[10] R. Cleaveland and B. Steffen, A linear-time model-checking algorithm for the alternation-free modal mu-calculus; in [19]. · Zbl 0772.68038
[11] Cormen, T.H.; Leiserson, C.E.; Rivest, R.L., Introduction to algorithms, (1990), McGraw-Hill New York · Zbl 1158.68538
[12] Dam, M., Translating CTL^{∗} into the modal μ-calculus, ()
[13] Dowling, W.F.; Gallier, J.H., Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. logic programming, 1, 267-284, (1984) · Zbl 0593.68062
[14] Emerson, E.A.; Lei, C.L., Efficient model checking in fragments of the propositional mu-calculus, (), 267-278
[15] Kozen, D., Results on the propositional mu-calculus, Theoret. comput. sci., 27, (1983) · Zbl 0553.03007
[16] Larsen, K.G., Proof systems for hennessy-milner logic with recursion, (), 215-230
[17] Larsen, K.G., Efficient local correctness checking, (), 30-43
[18] Larsen, K.G.; Godskesen, J.C.; Zeeberg, M., TAV — tools for automatic verification, ()
[19] ()
[20] Larsen, K.G.; Xinxin, L., Compositionality through an operational semantics of contexts, (), 526-539 · Zbl 0765.68107
[21] Stirling, C.; Walker, D., Local model checking in the modal mu-calculus, (), 369-383, Barcelona, Spain
[22] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific J. math., 5, 285-309, (1955) · Zbl 0064.26004
[23] Vergauwen, B.; Lewi, J., A linear algorithm for solving fixed-point equations on transition systems, (), 322-341
[24] Winskel, G., A note on model checking the modal v-calculus, (), 761-772
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.