More Web Proxy on the site http://driver.im/

article

Efficient on-the-fly model-checking for regular alternation-free mu-calculus

Authors:

Mihaela SighireanuAuthors Info & Claims

Science of Computer Programming, Volume 46, Issue 3

Pages 255 - 281

https://doi.org/10.1016/S0167-6423(02)00094-1

Published: 01 March 2003 Publication History

Abstract

Model-checking is a successful technique for automatically verifying concurrent finite-state systems. When designing a model-checker, a good compromise must be made between the expressive power of the property description formalism, the complexity of the model-checking problem, and the user-friendliness of the interface. We present a temporal logic and an associated model-checking method that attempt to fulfill these criteria. The logic is an extension of the alternation-free µ-calculus with ACTL-like action formulas and PDL-like regular expressions, allowing a concise and intuitive description of safety, liveness, and fairness properties over labeled transition systems. The model-checking method is based upon a succinct translation of the verification problem into a boolean equation system, which is solved by means of an efficient local algorithm having a good average complexity. The algorithm also allows to generate full diagnostic information (examples and counterexamples) for temporal formulas. This method is at the heart of the EVALUATOR 3.0 model-checker that we implemented within the CADP toolbox using the generic OPEN/CAESAR environment for on-the-fly verification.

References

[1]

{1} M. Aguilar Cornejo, H. Garavel, R. Mateescu, N. de Palma, Specification and verification of a dynamic reconfiguration protocol for agent-based applications, in: A. Laurentowski, J. Kosinski, Z. Mossurska, R. Ruchala (Eds.), Proc. 3rd IFIP WG 6.1 Internat. Working Conf. on Distributed Applications and Interoperable Systems DAIS'2001 (Krakow, Poland), Kluwer Academic Publishers, Dordrecht, 2001, pp. 229-242. Full version available as INRIA Research Report RR-4222.]]

Digital Library

[2]

{2} H.R. Andersen, Model checking and boolean graphs, Theoret. Comput. Sci. 126 (1) (1994) 3-30.]]

Digital Library

[3]

{3} A. Arnold, P. Crubillé, A linear algorithm to solve fixed-point equations on transition systems, Inform. Process. Lett. 29 (1988) 57-66.]]

Digital Library

[4]

{4} T. Arts, C. Benac Earle, Development of a verified Erlang program for resource locking, in: S. Gnesi, U. Ultes-Nitsche (Eds.), Proc. 6th Internat. Workshop on Formal Methods for Industrial Critical Systems FMICS'2001 (Paris, France), Univ. Paris 7-LIAFA and INRIA Rhône-Alpes, 2001, pp. 131-145.]]

[5]

{5} H. Bekic´, Definable operations in general algebras, and the theory of automata and flowcharts, in: C.B. Jones (Ed.), Programming Languages and their Definition, Lecture Notes in Computer Science, vol. 177, Springer, Berlin, 1984, pp. 30-55.]]

Digital Library

[6]

{6} J. Bradfield, Verifying Temporal Properties of Systems, Birkhäuser, Berlin, 1992.]]

Digital Library

[7]

{7} P.J.F. Carreira, M.E.F. Costa, Automatically verifying an object-oriented specification of the steam-boiler system, in: S. Gnesi, I. Schieferdecker, A. Rennoch (Eds.), Proc. 5th Internat. Workshop on Formal Methods for Industrial Critical Systems FMICS'2000 (Berlin, Germany), GMD Report 91, Berlin, 2000, pp. 345-360.]]

[8]

{8} E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Languages Systems 8 (2) (1986) 244-263.]]

Digital Library

[9]

{9} E.M. Clarke, K. McMillan, S. Campus, V. Hartonas-GarmHausen, symbolic model checking, in: R. Alur, T.A. Henzinger (Eds.), Proc. 8th Internat. Conf. on Computer-Aided Verification CAV'96 (New Brunswick, NJ, USA), Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, 1996, pp. 419-422.]]

Digital Library

[10]

{10} R. Cleaveland, B. Steffen, A linear-time model-checking algorithm for the alternation-free modal mu-calculus, in: K.G. Larsen, A. Skou (Eds.), Proc. 3rd Workshop on Computer Aided Verification CAV'91, Aalborg, Denmark, Lecture Notes in Computer Science, vol. 575, Springer, Berlin, 1991, pp. 48-58.]]

Digital Library

[11]

{11} P.F.G. Dechering, I.A. van Langevelde, Towards automated verification of splice in µCRL, Technical Report SEN-R0015, CWI, Amsterdam, 2000.]]

Digital Library

[12]

{12} P.F.G. Dechering, I.A. van Langevelde, On the verification of coordination, in: A. Porto, G.-C. Roman (Eds.), Proc. 4th Internat. Conf. on Coordination Models and Languages (Limassol, Cyprus), Lecture Notes in Computer Science, vol. 1906, Springer, Berlin, 2000, pp. 335-340.]]

Digital Library

[13]

{13} D.L. Dill, The Murø verification system, in: R. Alur, T.A. Henzinger (Eds.), Proc. 8th Internat. Conf. on Computer-Aided Verification CAV'96, New Brunswick, NJ, USA, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, 1996, pp. 390-393.]]

Digital Library

[14]

{14} Y. Dong, X. Du, Y.S. Ramakrishna, C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka, O. Sokolsky, E.W. Stark, D.S. Warren, Fighting livelock in the I-PROTOCOL: a comparative study of verification tools, in: R. Cleaveland (Ed.), Proc. 5th Internat. Conf. on Tools and Algorithms for the Construction and Analysis of Systems TACAS'99, Amsterdam, The Netherlands, Lecture Notes in Computer Science, vol. 1579, Springer, Berlin, 1999, pp. 74-88.]]

Digital Library

[15]

{15} M.B. Dwyer, G.S. Avrunin, J.C. Corbett, Patterns in property specifications for finite-state verification, in: Proc. 21st Internat. Conf. on Software Engineering ICSE'99, Los Angeles, CA, USA, 1999.]]

Digital Library

[16]

{16} E.A. Emerson, C.-L. Lei, Efficient model checking in fragments of the propositional mu-calculus, in: Proc. 1st LICS, 1986, pp. 267-278.]]

[17]

{17} A. Fantechi, S. Gnesi, F. Mazzanti, R. Pugliese, E. Tronci, A symbolic model checker for ACTL, in: D. Hutter, W. Stephan, P. Traverso, M. Ullmann (Eds.), Proc. Internat. Workshop on Current Trends in Applied Formal Methods FM-Trends'98, Boppard, Germany, Lecture Notes in Computer Science, vol. 1641, Springer, Berlin, 1998.]]

Digital Library

[18]

{18} J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, M. Sighireanu, (CADP CÆSAR/ALDEBARAN development package): a protocol validation and verification toolbox, in: R. Alur, T.A. Henzinger (Eds.), Proc. 8th Internat. Conf. on Computer-Aided Verification CAV'96, New Brunswick, NJ, USA, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, 1996, pp. 437-440.]]

Digital Library

[19]

{19} J.-C. Fernandez, C. Jard, T. Jéron, L. Nedelka, C. Viho, Using on-the-fly verification techniques for the generation of test suites, in: R. Alur, T.A. Henzinger (Eds.), Proc. 8th Internat. Conf. on Computer-Aided Verification CAV'96, New Brunswick, NJ, USA, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, 1996, pp. 348-359.]]

Digital Library

[20]

{20} J.-C. Fernandez, L. Mounier, A local checking algorithm for boolean equation systems, Report SPECTRE 95-07, VERIMAG, Grenoble, 1995.]]

[21]

{21} M.J. Fischer, R.E. Ladner, Propositional dynamic logic of regular programs, J. Comput. System Sci. 18 (1979) 194-211.]]

[22]

{22} H. Garavel, OPEN/CÆSAR: an open software architecture for verification, simulation, and testing in: B. Steffen (Ed.), Proc. 1st Internat. Conf. on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98, Lisbon, Portugal, Lecture Notes in Computer Science, vol. 1384, Springer, Berlin, 1998, pp. 68-84. Full version available as INRIA Research Report RR-3352.]]

Digital Library

[23]

{23} H. Garavel, J. Sifakis, Compilation and verification of LOTOS specifications, in: L. Logrippo, R.L. Probert, H. Ural (Eds.), Proc. 10th IFIP Internat. Symp. on Protocol Specification, Testing and Verification, Ottawa, Canada, 1990, pp. 379-394.]]

Digital Library

[24]

{24} J.-F. Groote, J. Pang, A. Wouters, A balancing act: analyzing a distributed lift system, in: S. Gnesi, U. Ultes-Nitsche (Eds.), Proc. 6th Internat. Workshop on Formal Methods for Industrial Critical Systems FMICS'2001 (Paris, France), Univ. Paris 7-LIAFA and INRIA Rhône-Alpes, pp. 1-12. Full version available as CWI Report SEN-R0111.]]

[25]

{25} J.-F. Groote, A. Ponse, The syntax and semantics of µCRL, Technical Report CS-R9076, CWI, Amsterdam, 1990.]]

[26]

{26} K. Hamaguchi, H. Hiraishi, S. Yajima, Branching time regular temporal logic for model checking with linear time complexity, in: E.M. Clarke, R.P. Kurshan (Eds.), Proc. 2nd Internat. Conf. on Computer-Aided Verification CAV'90, New Brunswick, NJ, USA, Lecture Notes in Computer Science, vol. 531, Springer, Berlin, 1990, pp. 253-262.]]

Digital Library

[27]

{27} R.H. Hardin, Z. Har'El, R.P. Kurshan, COSPAN, in: R. Alur, T.A. Henzinger (Eds.), Proc. 8th Internat. Conf. on Computer-Aided Verification CAV'96, New Brunswick, NJ, USA, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, 1996, pp. 423-427.]]

[28]

{28} G. Holzmann, The model checker SPIN, IEEE Trans. Software Eng. 23 (5) (1997) 279-295.]]

Digital Library

[29]

{29} A. Ingolfsdottir, B. Steffen, Characteristic formulae for processes with divergence, Inform. Comput. 110 (1) (1994) 149-163.]]

Digital Library

[30]

{30} ISO/IEC, LOTOS-a Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, International Standard 8807, International Organization for Standardization--Information Processing Systems--Open Systems Interconnection, Genève, 1988.]]

[31]

{31} D. Kozen, Results on the propositional µ-calculus, Theoret. Comput. Sci. 27 (1983) 333-354.]]

[32]

{32} K.G. Larsen, Proof systems for Hennessy-Milner logic with recursion, in: Proc. 13th Colloq. on Trees in Algebra and Programming CAAP'88, Nancy, France, Lecture Notes in Computer Science, vol. 299, Springer, Berlin, 1988, pp. 215-230.]]

Digital Library

[33]

{33} X. Liu, C.R. Ramakrishnan, S.A. Smolka, Fully local and efficient evaluation of alternating fixed points, in: B. Steffen (Ed.), Proc. 1st Internat. Conf. on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98, Lisbon, Portugal, Lecture Notes in Computer Science, vol. 1384, Springer, Berlin, 1998, pp. 5-19.]]

Digital Library

[34]

{34} L. Logrippo, L. Andriantsiferana, B. Ghribi, Prototyping and formal requirement validation of GPRS: a mobile data packet radio service for GSM, in: C.B. Weinstock, J. Rushby (Eds.), Proc. 7th IFIP Internat. Working Conf. on Dependable Computing for Critical Applications DCCA-7, San Jose, CA, USA, 1999.]]

Digital Library

[35]

{35} A. Mader, Verification of Modal Properties Using Boolean Equation Systems, VERSAL 8, Bertz Verlag, Berlin, 1997.]]

[36]

{36} Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, vol. I (Specification), Springer, Berlin, 1992.]]

Digital Library

[37]

{37} R. Mateescu, Local model-checking of an alternation-free value-based modal mu-calculus, in: A. Bossi, A. Cortesi, F. Levi (Eds.), Proc. 2nd Internat. Workshop on Verification, Model Checking and Abstract Interpretation VMCAI'98, Pisa, Italy, University Ca' Foscari of Venice, 1998.]]

[38]

{38} R. Mateescu, Efficient diagnostic generation for boolean equation systems, in: S. Graf, M. Schwartzbach (Eds.), Proc. 6th Internat. Conf. on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2000, Berlin, Germany, Lecture Notes in Computer Science, vol. 1785, Springer, Berlin, 2000, pp. 251-265, Full version available as INRIA Research Report RR-3861.]]

Digital Library

[39]

{39} R.D. Nicola, F.W. Vaandrager, Action versus state based logics for transition systems, in: I. Guessarian (Ed.), Semantics of Systems of Concurrent Processes (La Roche Posay, France), Lecture Notes in Computer Science, vol. 469, Springer, Berlin, 1990, pp. 407-419.]]

Digital Library

[40]

{40} Y.S. Ramakrishna, C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka, T.W. Swift, D.S. Warren, Efficient model checking using tabled resolution, in: Proc. 9th Internat. Conf. on Computer-Aided Verification CAV'97, Haifa, Israel, Lecture Notes in Computer Science, vol. 1254, Springer, Berlin, 1997, pp. 143-154.]]

Digital Library

[41]

{41} M. Sage, C. Johnson, A declarative prototyping environment for the development of multi-user safety-critical systems, in: Proc. 17th Internat. System Safety Conf. ISSC'99, Orlando, Florida, USA, System Safety Society, 1999.]]

[42]

{42} D. Simon, B. Espiau, K. Kapellos, R. Pissard-Giboll, et al., The ORCCAD Architecture, Internat. J. Robot. Res. 17 (4) (1998) 338-359.]]

[43]

{43} R. Streett, Propositional dynamic logic of looping and converse, Inform. Control 54 (1982) 121-141.]]

[44]

{44} W. Thomas, Computation tree logic and regular ω-languages, in: G. Rozenberg, J.W. de Bakker, W.-P. de Roever (Eds.), Linear Time, Branching Time and Partial Order in Logics and Models of Concurrency, Lecture Notes in Computer Science, vol. 354, Springer, Berlin, 1989, pp. 690-713.]]

Digital Library

[45]

{45} E. Tronci, Hardware verification, boolean logic programming, boolean functional programming, in: Proc. 10th Ann. IEEE Symp. on Logic in Computer Science LICS'95, San Diego, CA, IEEE Computer Society Press, Silver Spring, MD, 1995, pp. 408-418.]]

Digital Library

[46]

{46} M.Y. Vardi, P. Wolper, Reasoning about infinite computations, Inform. Comput. 115 (1) (1994) 1-37.]]

Digital Library

[47]

{47} B. Vergauwen, J. Lewi, Efficient local correctness checking for single and alternating boolean equation systems, in: S. Abiteboul, E. Shamir (Eds.), Proc. 21st ICALP, Vienna, Austria, Lecture Notes in Computer Science, vol. 820, Springer, Berlin, 1994, pp. 304-315.]]

Digital Library

[48]

{48} P. Wolper, Temporal logic can be more expressive, Inform. Control 56 (1/2) (1983) 72-99.]]

[49]

{49} P. Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, in: Proc. 24th IEEE Symp. on Foundations of Computer Science FOCS'83, Tucson, Arizona, USA, 1983, pp. 185-194.]]

Digital Library

Cited By

Faqrizal ISalaün GFalcone Y(2024)Adaptive Industrial Control Systems via IEC 61499 and Runtime EnforcementACM Transactions on Autonomous and Adaptive Systems10.1145/369134519:4(1-31)Online publication date: 31-Aug-2024
https://dl.acm.org/doi/10.1145/3691345
Cleaveland RKeiren JFontana P(2024)An Expressive Timed Modal Mu-Calculus for Timed AutomataQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-68416-6_10(160-178)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68416-6_10
Cleaveland RKeiren J(2023)Extensible Proof Systems for Infinite-State SystemsACM Transactions on Computational Logic10.1145/362278625:1(1-60)Online publication date: 18-Nov-2023
https://dl.acm.org/doi/10.1145/3622786
Show More Cited By

Index Terms

Efficient on-the-fly model-checking for regular alternation-free mu-calculus
1. Software and its engineering
  1. Software creation and management
    1. Software development process management
      1. Software development methods
2. Theory of computation
  1. Computational complexity and cryptography
    1. Complexity classes
  2. Semantics and reasoning
    1. Program semantics

Recommendations

CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems
Special section on Tools and Algorithms for the Construction and Analysis of Systems

Boolean equation systems (Bess) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking and model checking. These problems can be solved on the fly (i.e., without ...
Distributed Symbolic Model Checking for μ-Calculus

In this paper we propose a distributed symbolic algorithm for model checking of propositional -calculus formulas. -calculus is a powerful formalism and -calculus model checking can solve many problems, including, for example, verification of (fair) CTL ...
Regular model checking for LTL(MSO)

Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Science of Computer Programming

Science of Computer Programming Volume 46, Issue 3

Special issure on formal methods for industrial critical systems (FMICS 2000)

March 2003

110 pages

ISSN:0167-6423

Issue’s Table of Contents

Publisher

Elsevier North-Holland, Inc.

United States

Publication History

Published: 01 March 2003

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

47
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Faqrizal ISalaün GFalcone Y(2024)Adaptive Industrial Control Systems via IEC 61499 and Runtime EnforcementACM Transactions on Autonomous and Adaptive Systems10.1145/369134519:4(1-31)Online publication date: 31-Aug-2024
https://dl.acm.org/doi/10.1145/3691345
Cleaveland RKeiren JFontana P(2024)An Expressive Timed Modal Mu-Calculus for Timed AutomataQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-68416-6_10(160-178)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68416-6_10
Cleaveland RKeiren J(2023)Extensible Proof Systems for Infinite-State SystemsACM Transactions on Computational Logic10.1145/362278625:1(1-60)Online publication date: 18-Nov-2023
https://dl.acm.org/doi/10.1145/3622786
Laveaux MWesselink WWillemse T(2022)On-The-Fly Solving for Symbolic Parity GamesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-99527-0_8(137-155)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-030-99527-0_8
Hashmi MGovernatori GLam HWynn M(2018)Are we done with business process complianceKnowledge and Information Systems10.1007/s10115-017-1142-157:1(79-133)Online publication date: 1-Oct-2018
https://dl.acm.org/doi/10.1007/s10115-017-1142-1
Mateescu RRequeno J(2018)On-the-fly model checking for extended action-based probabilistic operatorsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-018-0499-020:5(563-587)Online publication date: 1-Oct-2018
https://dl.acm.org/doi/10.1007/s10009-018-0499-0
Yousefi BGhassemi FKhosravi R(2017)Modeling and efficient verification of wireless ad hoc networksFormal Aspects of Computing10.1007/s00165-017-0429-z29:6(1051-1086)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.1007/s00165-017-0429-z
Pham LNguyen THung NThang HDe Raedt LDeville YBui MLinh TSang DPhuong NOanh N(2016)AutoBotProceedings of the 7th Symposium on Information and Communication Technology10.1145/3011077.3011131(403-410)Online publication date: 8-Dec-2016
https://dl.acm.org/doi/10.1145/3011077.3011131
Madeira ANeves RBarbosa LMartins M(2016)A method for rigorous design of reconfigurable systemsScience of Computer Programming10.1016/j.scico.2016.05.001132:P1(50-76)Online publication date: 15-Dec-2016
https://dl.acm.org/doi/10.1016/j.scico.2016.05.001
Lockefeer LWilliams DFokkink W(2016)Formal specification and verification of TCP extended with the Window Scale OptionScience of Computer Programming10.1016/j.scico.2015.08.005118:C(3-23)Online publication date: 1-Mar-2016
https://dl.acm.org/doi/10.1016/j.scico.2015.08.005
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents