Abstract
In this paper, we present the constraint language Toupie which is a finite domain μ-calculus interpreter that uses extended decision diagrams to represent relations and formulae. “Classical” constraint logic programming languages over finite domains (CLP(FD)) are designed to find one solution to a constraint problem, eventually the best one according to a given criterion. In Toupie, constraints are used to characterize existing relationships between variables. We advocate the use of this paradigm to model and solve efficiently difficult constraint problems that are not tractable with CLP(FD) languages.
Chapter PDF
Similar content being viewed by others
References
A. Arnold. MEC: a System for Constructing and Analysing Transition Systems. In Workshop on Automatic Verification Methods for Finite State Systems, June 1989.
J.R. Burch, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. IEEE transactions on computers, 1990.
A. Bouali. Etudes et mises en œuvre d'outils de vérification basée sur la bisimulation. PhD thesis, Université Paris VII, 03 1993. in french.
R. Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. ACM Computing Surveys, 1992.
W. Buettner and H. Simonis. Embedding Boolean Expressions into Logic Programming. Journal of Symbolic Computation, 4:191–205, 1987.
R. Cousot and P. Cousot. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. research report LIX/RR/92/09, Ecole Polytechnique, 1992.
M-M. Corsini, B. Le Charlier, K. Musumbu, and A. Rauzy. Efficient Abstract Interpretation of Prolog Programs by means of Constraint Solving over Finite Domains (extended abstract). In Proceedings of the 5th Int. Symposium on Programming Language Implementation and Logic Programming, PLILP'93, Estonie, 1993.
M-M. Corsini, A. Griffault, and A. Rauzy. Yet another Application for Toupie: Verification of Mutual Exclusion Algorithms. In proceedings of Logic Programming and Automated Reasonning, LPAR'93. LNCS, 1993.
A. Colmerauer. An introduction to prologIII. Communications of the ACM, 28 (4), July 1990.
M-M. Corsini and A. Rauzy. First Experiments with Toupie. Technical Report 577-93, LaBRI — Université Bordeaux I, 1993.
R. Enders, T. Filkorn, and D. Taubner. Generating BDDs for Symbolic Model Checking in CCS. Journal of Distributed Computing, 6:155–164, June 1993.
P. Van Hentenryck. Constraint Handling in Logic Programming. Logic Programming. MIT Press, 1990.
J. Jaffar and J.L. Lassez. Constraint logic programming. In Proceedings of Principle of Programming Languages (POPL'87), January 1987.
R. Milner. Communication and Concurrency. Prentice Hall, New York, 1989.
J. Ullman. Implementation of logical query languages for databases. ACM Transactions on Database Systems, 10, 03 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Corsini, M.M., Rauzy, A. (1994). Symbolic model checking and constraint logic programming: A cross-fertilization. In: Sannella, D. (eds) Programming Languages and Systems — ESOP '94. ESOP 1994. Lecture Notes in Computer Science, vol 788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57880-3_12
Download citation
DOI: https://doi.org/10.1007/3-540-57880-3_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57880-2
Online ISBN: 978-3-540-48376-2
eBook Packages: Springer Book Archive