Abstract
Boolean Equation Systems (Bess) provide a useful framework for the verification of concurrent finite-state systems. In practice, it is desirable that a Bes resolution also yields diagnostic information explaining, preferably in a concise way, the truth value computed for a given variable of the Bes. Using a representation of Bess as extended boolean graphs (Ebgs), we propose a characterization of full diagnostics (i.e., both examples and counterexamples) as a particular class of subgraphs of the Ebg associated to a Bes. We provide algorithms that compute examples and counterexamples in linear time and can be straightforwardly used to extend known (global or local) Bes resolution algorithms with diagnostic generation facilities.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
References
H. R. Andersen. Model Checking and Boolean Graphs. TCS, 126(1):3–30, 1994. 251, 254, 257, 259, 263
H. R. Andersen and B. Vergauwen. Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion. In P. Wolper, editor, Proceedings of CAV’95 (Liege, Belgium), vol. 939 of LNCS, pp. 142–154. Springer Verlag, July 1995. 251, 263
A. Arnold and P. Crubillé. A Linear Algorithm to Solve Fixed-point Equations on Transition Systems. Information Processing Letters, 29:57–66, 1988. 251, 257, 259, 263
M. Bozga, J-C. Fernandez, A. Kerbrat, and L. Mounier. Protocol Verification with the ALDEBARAN toolset. Springer International Journal on Software Tools for Technology Transfer (STTT), 1(1–2):166–183, 1997. 252
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986. 251, 252, 263
E. M. Clarke, O. Grumberg, K. L. McMillan, and X. Zhao. Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. In Proceedings of DAC’95 (San Francisco, CA, USA), pp. 427–432. ACM, June 1995. 252
E. M. Clarke, O. Grumberg, and D. Long. Verification Tools for Finite-State Concurrent Systems. In J. W. de Bakker, W-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX School/Symposium (Noordwijkerhout, The Netherlands), vol. 803 of LNCS, pp. 124–175. Springer Verlag, June 1993. 252
R. Cleaveland. On Automatically Explaining Bisimulation Inequivalence. In E. M. Clarke and R. P. Kurshan, editors, Proceedings of CAV’90 (New Brunswick, NJ, USA), vol. 531 of LNCS, pp. 364–372. Springer Verlag, June 1990. 252
R. Cleaveland and B. Steffen. A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. In K. G. Larsen and A. Skou, editors, Proceedings of CAV’91 (Aalborg, Denmark), vol. 575 of LNCS, pp. 48–58. Springer Verlag, July 1991. 251, 252, 254, 257, 259, 263
E. A. Emerson and C-L. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In Proceedings of the 1st LICS, pp. 267–278, 1986. 253
J-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP (CÆSAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In R. Alur and T. A. Henzinger, editors, Proceedings of CAV’96 (New Brunswick, NJ, USA), vol. 1102 of LNCS, pp. 437–440. Springer Verlag, August 1996. 263
J-C. Fernandez, C. Jard, T. Jéron, L. Nedelka, and C. Viho. Using On-the-Fly Verification Techniques for the Generation of Test Suites. In R. Alur and T. A. Henzinger, editors, Proceedings of CAV’96 (New Brunswick, NJ, USA), vol. 1102 of LNCS, pp. 348–359. Springer Verlag, August 1996. 263
J-C. Fernandez and L. Mounier. “On the Fly” Verification of Behavioural Equivalences and Preorders. In K. G. Larsen and A. Skou, editors, Proceedings of CAV’91 (Aalborg, Denmark), vol. 575 of LNCS. Springer Verlag, July 1991. 252
H. Garavel. OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing. In B. Steffen, editor, Proceedings of TACAS’98 (Lisbon, Portugal), vol. 1384 of LNCS, pp. 68–84. Springer Verlag, March 1998. 263
H. Korver. Computing Distinguishing Formulas for Branching Bisimulation. In K. G. Larsen and A. Skou, editors, Proceedings of CAV’91 (Aalborg, Denmark), vol. 575 of LNCS, pp. 13–23. Springer Verlag, July 1991. 252
D. Kozen. Results on the Propositional μ-calculus. TCS, 27:333–354, 1983. 252
K. G. Larsen. Efficient Local Correctness Checking. In G. v. Bochmann and D. K. Probst, editors, Proceedings of CAV’92 (Montréal, Canada), vol. 663 of LNCS, pp. 30–43. Springer Verlag, June–July 1992. 251
X. Liu, C. R. Ramakrishnan, and S. A. Smolka. Fully Local and Efficient Evaluation of Alternating Fixed Points. In B. Steffen, editor, Proceedings of TACAS’98 (Lisbon, Portugal), vol. 1384 of LNCS. Springer Verlag, March 1998. 251, 263
X. Liu and S. A. Smolka. Simple Linear-Time Algorithms for Minimal Fixed Points. In K. G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of ICALP’98 (Aalborg, Denmark), vol. 1443 of LNCS. Springer Verlag, July 1998. 251, 259, 263
A. Mader. Verification of Modal Properties Using Boolean Equation Systems. VERSAL 8, Bertz Verlag, Berlin, 1997. 251, 254, 263
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. 252
R. De Nicola and F.W. Vaandrager. Action versus State based Logics for Transition. Systems. In Proceedings Ecole de Printemps on Semantics of Concurrency, vol. 469 of LNCS, pp. 407–419. Springer Verlag, 1990. 263
A. Rasse. Error Diagnosis in Finite Communicating Systems. In K. G. Larsen and A. Skou, editors, Proceedings of CAV’91 (Aalborg, Denmark), vol. 575 of LNCS, pp. 114–124. Springer Verlag, July 1991. 252
P. Stevens and C. Stirling. Practical Model-Checking using Games. In B. Steffen, editor, Proceedings of TACAS’98 (Lisbon, Portugal), vol. 1384 of LNCS, pp. 85–101. Springer Verlag, March 1998. 252
C. Stirling. Bisimulation, model checking and other games. In Notes for Mathfit instructional meeting on games and computation, Edinburgh, June 1997. 252
R. Streett. Propositional Dynamic Logic of Looping and Converse. Information and Control, (54):121–141, 1982. 263
A. Tarski. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, (5):285–309, 1955. 262
B. Vergauwen and J. Lewi. A Linear Algorithm for Solving Fixed-point Equations on Transition Systems. In Proceedings of CAAP’92 (Rennes, France), vol. 581 of LNCS, pp. 322–341. Springer Verlag, February 1992. 251, 257, 259, 263
B. Vergauwen and J. Lewi. Efficient Local Correctness Checking for Single and Alternating Boolean Equation Systems. In S. Abiteboul and E. Shamir, editors, Proceedings of ICALP’94 (Vienna), vol. 820 of LNCS, pp. 304–315. Springer Verlag, July 1994. 251, 259, 263
B. Vergauwen, J. Wauman, and J. Lewi. Efficient FixPoint Computation. In Proceedings of SAS’94 (Namur, Belgium), vol. 864 of LNCS, pp. 314–328. Springer Verlag, September 1994. 251, 257, 259
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mateescu, R. (2000). Efficient Diagnostic Generation for Boolean Equation Systems. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_18
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive