TY - GEN

T1 - Parameterised Boolean equation systems (Extended abstract)

AU - Groote, J.F.

AU - Willemse, T.A.C.

PY - 2004

Y1 - 2004

N2 - Boolean equation system are a useful tool for verifying formulas from modal mu-calculus on transition systems (see [9] for an excellent treatment). We are interested in an extension of boolean equation systems with data. This allows to formulate and prove a substantially wider range of properties on much larger and even infinite state systems. In previous works [4,6] it has been outlined how to transform a modal formula and a process, both containing data, to a so-called parameterised boolean equation system, or equation system for short. In this article we focus on techniques to solve such equation systems.
We introduce a new equivalence between equation systems, because existing equivalences are not compositional. We present techniques similar to Gauß elimination as outlined in [9] that allow to solve each equation system provided a single equation can be solved. We give several techniques for solving single equations, such as approximation (known), patterns (new) and invariants (new). Finally, we provide several small but illustrative examples of verifications of modal mu-calculus formulas on concrete processes to show the use of the techniques.

AB - Boolean equation system are a useful tool for verifying formulas from modal mu-calculus on transition systems (see [9] for an excellent treatment). We are interested in an extension of boolean equation systems with data. This allows to formulate and prove a substantially wider range of properties on much larger and even infinite state systems. In previous works [4,6] it has been outlined how to transform a modal formula and a process, both containing data, to a so-called parameterised boolean equation system, or equation system for short. In this article we focus on techniques to solve such equation systems.
We introduce a new equivalence between equation systems, because existing equivalences are not compositional. We present techniques similar to Gauß elimination as outlined in [9] that allow to solve each equation system provided a single equation can be solved. We give several techniques for solving single equations, such as approximation (known), patterns (new) and invariants (new). Finally, we provide several small but illustrative examples of verifications of modal mu-calculus formulas on concrete processes to show the use of the techniques.

U2 - 10.1007/978-3-540-28644-8_20

DO - 10.1007/978-3-540-28644-8_20

M3 - Conference contribution

SN - 3-540-22940-X

T3 - Lecture Notes in Computer Science

SP - 308

EP - 324

BT - CONCUR 2004 - concurrency theory : proceedings 15th international conference, London, UK, August 31-September 3, 2004

A2 - Gardner, Ph.

A2 - Yoshida, N.

PB - Springer

CY - Berlin

ER -