Abstract
Toupie is a finite domain μ-calculus model checker that uses extended decision diagrams to represent relations and formulae. In recent papers, we have demonstrated that such a language can model and solve difficult problems, such as AI Puzzles, Abstract Interpretation of Logic Programs with very good running times. Hereafter we show how, in Toupie, one can handle transition systems and check properties of Mutual Exclusion Algorithms.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
D. Park. Finitiness is Mu-ineffable. Theory of Computation, 3, 1974.
J.R. Burch, E.M. Clarke, and K.L. Mc Millan. Symbolic Model Checking: 1020 States and Beyond. In 5th Annual IEEE Symposium on Logic in Computer Science, pages 428–439. IEEE, 1990.
M-M. Corsini, K. Musumbu, and A. Rauzy. The μ-calculus over Finite Domains as an Abstract Semantics of Prolog. In M. Billaud, P. Castéran, M-M. Corsini, K. Musumbu, and A. Rauzy, editors, WSA '92 Workshop on Static Analysis (Bordeaux), volume 81–82 of Bigre, pages 51–59. Atelier Irisa, Sept. 23–25 1992.
M-M. Corsini and A. Rauzy. First Experiments with Toupie, 1993. submitted to ILPS'93.
R. Bryant. Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35:677–691, 8 1986.
K. Brace, R. Rudell, and R. Bryant. Efficient Implementation of a BDD Package. In 27th ACM/IEEE Design Automation Conference. IEEE 0738, 1990.
G.L. Peterson. MYTHS about the Mutual Exclusion Problem. Information Processing Letters, 12(3):115–116, June 1981.
A. Arnold. MEC: a System for Constructing and Analysing Transition Systems. In Workshop on Automatic Verification Methods for Finite State Systems, June 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Corsini, MM., Griffault, A., Rauzy, A. (1993). Yet another application for Toupie: Verification of mutual exclusion algorithms. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1993. Lecture Notes in Computer Science, vol 698. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56944-8_44
Download citation
DOI: https://doi.org/10.1007/3-540-56944-8_44
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56944-2
Online ISBN: 978-3-540-47830-0
eBook Packages: Springer Book Archive