Abstract
In model checking for temporal logic, the correctness of a (concurrent) system with respect to a desired behavior is verified by checking whether a structure that models the system satisfies a formula describing the behaviour. Most existing verification techniques, and in particular those defined for concurrent calculi like as CCS, are based on a representation of the concurrent system by means of a labelled transition system. In this approach to verification, state explosion is one of the most serious problems. In this paper we present a new temporal logic, the selective mu-calculus, with the property that only the actions occurring in a formula are relevant to check the formula itself. We prove that the selective mu-calculus is as powerful as the mu-calculus. We define the notion of ρ-bisimulation between transition systems: given a set of actions p,a transition system ρ-bisimulates another one if they have the same behaviour with respect to the actions in p. We prove that, if two transition systems are ρ-equivalent, they preserve all the selective mu-calculus formulae with occurring actions in ρ. Consequently, a formula with occurring actions ρ can be more efficiently checked on a transition system ρ-equivalent to the standard one, but smaller than it.
Keywords
Download to read the full chapter text
Chapter PDF
References
A. Aziz, T.R. Shiple, V. Singhal, A.L. Sangiovanni-Vincentelli. Formula-Dependent Equivalence for Compositional CTL Model Checking. In Proceedings of Workshop on Computer Aided Verification (CAV’94), LNCS 818, 1994. 324–337.
R. Barbuti, N. De Francesco, A. Santone, G. Vaglini. Formula-Based Reduction of Transition Systems. Internal Report IR-3/97, Dipartimento di Ingegneria dell’Informazione, Univ. of Pisa.
S. Bensalem, A. Bouajjani, C. Loiseaux, J. Sifakis. Property Preserving Simulations. In Proceedings of Workshop on Computer Aided Verification (CAV’92), LNCS 663, 1992. 260–273.
O. Bernholtz, M.Y. Vardi, P. Wolper. An Automata-Theoretic Approach to Branching- Time Model Checking. In Proceedings of Workshop on Computer Aided Verification (CAV’94), LNCS 818, 1994. 142–155.
A. Bouajjani, J.C. Fernandez, S. Graf, C. Rodriguez, J. Sifakis. “Safety for Branching Time Semantics”. In Proceedings of the 18th International Colloquium on Automata, Languages and Programming LNCS 510, 1991. 76–92.
G. Bruns. A Case Study in Safety-Critical Design. In Proceedings of Workshop on Computer Aided Verification (CAV’92), LNCS 663, 1992. 220–233.
G. Bruns. A Practical Technique for Process Abstraction. In Proceedings of International Conference on Concurrency Theory (CONCUR’93), LNCS 714, 1993. 37–49.
R. Cleaveland, J. Parrow, B. Steffen. The concurrency workbench: operating instructions. Tech. Notes Sussex University, 1988.
C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis. Memory Efficient Algorithms for the Verification of Temporal Properties. In Workshop on Computer Aided Verification, DIMACS 90, June 1990.
D. Dams, O. Grumberg, R. Gerth. Generation of reduced models for checking fragments of CTL. In Proceedings of Workshop on Computer Aided Verification (CAV’93), LNCS 697, 1993. 479–490.
N. De Francesco, A. Santone, G. Vaglini. A Non-Standard Semantics for Generating Reduced Transition Systems. In Proceedings of LOMAPS’96, LNCS 1192, 1996. 370–387.
R. De Simone, D. Vergamini. Aboard AUTO. INRIA Technical Report 111, 1989.
R. De Simone, A. Ressouche. Compositional semantics of ESTEREL and verification by compositional reductions. In Proceedings of Workshop on Computer Aided Verification (CAV’94), LNCS 818, 1994. 441–454.
J. C. Fernandez, A. Kerbrat, L. Mounier. Symbolic Equivalence Checking. In Proceedings of the 5th International Conference on Computer-Aided Verification, LNCS 697, 1993. 85–96.
J. C. Fernandez, L. Mounier. Verifying bisimulation on the fly. In Third International Conference on Formal Description Techniques, FORTE’90, Madrid, November 1990.
J.C. Fernandez, L. Mounier. “On th Fly” Verification of Behavioural Equivalences and Preorders. In Proceedings of the Third International Conference on Computer-Aided Verification, LNCS 575, 1991. 181–191.
J.C. Fernandez et al. “CADP A Protocol Validation and Verification Toolbox”. In Proceedings of the Third International Conference on Computer-Aided Verification, LNCS 1102, 1996. 437–440.
T. A. Henzinger, O. Kupferman, M.Y. Vardi. A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking. In Proceedings of International Conference on Concurrency Theory (CONCUR’96), LNCS 1119, 1996. 514–529.
C. Jard, T. Jéron. On-Line Model-Checking for Finite Linear Temporal Logic Specifications. In International Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, 1989. 189–196.
C. Jard, T. Jéron. Bounded-memory Algorithms for Verification Onthe-fly. In Proceedings of the Third International Conference on Computer-Aided Verification, LNCS 575, 1991. 192–201.
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27, (1983). 333–354.
Y.S. Kwong. On reduction of asynchronous systems. Theoretical Computer Science 5, 1977. 25–50.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
D. Peled. All from one, one for all, on model-checking using representatives. In Proceedings of the Fifth International Conference on Computer-Aided Verification(CAV’93), LNCS 679, 1993. 409–423.
D. Peled. Combining Partial Order Reductions with On-the Fly Model-Checking. In Proceedings of the 6th International Conference on Computer-Aided Verification(CAV’94), LNCS 818, 1994. 377–390.
J. Sifakis. Property Preserving Homomorphisms of Transition Systems. In Logics of Programs, LNCS 164, 1983.
C. Stirling. An Introduction to modal and temporal logics for CCS In Concurrency: Theory, Language, and Architecture, LNCS 391, 1989.
A. Valmari. A stubborn attack on state explosion. In Proceedings of International Conference on Computer-Aided Verification (CAV’90), LNCS 531, 1990. 156–165.
A. Valmari, M. Clegg. Reduced Labelled Transition Systems Save Verification Effort. In Proceedings of the International Conference on Concurrency Theory (CONCUR’91), LNCS, 1991. 526–540.
M. Y. Vardi, P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic Computer Science, Cambridge, 1986. 322–331
M. Y. Vardi, P. Wolper. An automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32 (2): 18221, April 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Barbuti, R., De Francesco, N., Santone, A., Vaglini, G. (1997). Selective mu-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds) Formal Description Techniques and Protocol Specification, Testing and Verification. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35271-8_32
Download citation
DOI: https://doi.org/10.1007/978-0-387-35271-8_32
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5260-1
Online ISBN: 978-0-387-35271-8
eBook Packages: Springer Book Archive