Modal µ-Calculus, Model Checking and Gauß Elimination

Hendrik Brinksma (Editor), Angelika H. Mader, W.R. Cleaveland (Editor), K.G. Larsen (Editor), K.G. Larsen (Editor), T. Margaria (Editor), B. Steffen (Editor)

Research output: Contribution to conferencePaperAcademicpeer-review

17 Downloads (Pure)

Abstract

In this paper we present a novel approach for solving Boolean equation systems with nested minimal and maximal fixpoints. The method works by successively eliminating variables and reducing a Boolean equation system similar to Gauß elimination for linear equation systems. It does not require backtracking techniques. Within one framework we suggest a global and a local algorithm. In the context of model checking in the modal-calculus the local algorithm is related to the tableau methods, but has a better worst case complexity.
Original languageUndefined
Pages72-88
Number of pages17
DOIs
Publication statusPublished - May 1995
EventFirst International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995 - Aarhus, Denmark
Duration: 19 May 199520 May 1995
Conference number: 1

Workshop

WorkshopFirst International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995
Abbreviated titleTACAS
CountryDenmark
CityAarhus
Period19/05/9520/05/95

Keywords

  • IR-56275
  • EWI-1156

Cite this

Brinksma, H. (Ed.), Mader, A. H., Cleaveland, W. R. (Ed.), Larsen, K. G. (Ed.), Larsen, K. G. (Ed.), Margaria, T. (Ed.), & Steffen, B. (Ed.) (1995). Modal µ-Calculus, Model Checking and Gauß Elimination. 72-88. Paper presented at First International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995, Aarhus, Denmark. https://doi.org/10.1007/3-540-60630-0_4
Brinksma, Hendrik (Editor) ; Mader, Angelika H. ; Cleaveland, W.R. (Editor) ; Larsen, K.G. (Editor) ; Larsen, K.G. (Editor) ; Margaria, T. (Editor) ; Steffen, B. (Editor). / Modal µ-Calculus, Model Checking and Gauß Elimination. Paper presented at First International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995, Aarhus, Denmark.17 p.
@conference{543df319dc3241c1a658c7e639bd22ed,
title = "Modal µ-Calculus, Model Checking and Gau{\ss} Elimination",
abstract = "In this paper we present a novel approach for solving Boolean equation systems with nested minimal and maximal fixpoints. The method works by successively eliminating variables and reducing a Boolean equation system similar to Gau{\ss} elimination for linear equation systems. It does not require backtracking techniques. Within one framework we suggest a global and a local algorithm. In the context of model checking in the modal-calculus the local algorithm is related to the tableau methods, but has a better worst case complexity.",
keywords = "IR-56275, EWI-1156",
author = "Hendrik Brinksma and Mader, {Angelika H.} and W.R. Cleaveland and K.G. Larsen and K.G. Larsen and T. Margaria and B. Steffen",
note = "Imported from DIES; null ; Conference date: 19-05-1995 Through 20-05-1995",
year = "1995",
month = "5",
doi = "10.1007/3-540-60630-0_4",
language = "Undefined",
pages = "72--88",

}

Brinksma, H (ed.), Mader, AH, Cleaveland, WR (ed.), Larsen, KG (ed.), Larsen, KG (ed.), Margaria, T (ed.) & Steffen, B (ed.) 1995, 'Modal µ-Calculus, Model Checking and Gauß Elimination' Paper presented at First International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995, Aarhus, Denmark, 19/05/95 - 20/05/95, pp. 72-88. https://doi.org/10.1007/3-540-60630-0_4

Modal µ-Calculus, Model Checking and Gauß Elimination. / Brinksma, Hendrik (Editor); Mader, Angelika H.; Cleaveland, W.R. (Editor); Larsen, K.G. (Editor); Larsen, K.G. (Editor); Margaria, T. (Editor); Steffen, B. (Editor).

1995. 72-88 Paper presented at First International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995, Aarhus, Denmark.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

T1 - Modal µ-Calculus, Model Checking and Gauß Elimination

AU - Mader, Angelika H.

A2 - Brinksma, Hendrik

A2 - Cleaveland, W.R.

A2 - Larsen, K.G.

A2 - Larsen, K.G.

A2 - Margaria, T.

A2 - Steffen, B.

N1 - Imported from DIES

PY - 1995/5

Y1 - 1995/5

N2 - In this paper we present a novel approach for solving Boolean equation systems with nested minimal and maximal fixpoints. The method works by successively eliminating variables and reducing a Boolean equation system similar to Gauß elimination for linear equation systems. It does not require backtracking techniques. Within one framework we suggest a global and a local algorithm. In the context of model checking in the modal-calculus the local algorithm is related to the tableau methods, but has a better worst case complexity.

AB - In this paper we present a novel approach for solving Boolean equation systems with nested minimal and maximal fixpoints. The method works by successively eliminating variables and reducing a Boolean equation system similar to Gauß elimination for linear equation systems. It does not require backtracking techniques. Within one framework we suggest a global and a local algorithm. In the context of model checking in the modal-calculus the local algorithm is related to the tableau methods, but has a better worst case complexity.

KW - IR-56275

KW - EWI-1156

U2 - 10.1007/3-540-60630-0_4

DO - 10.1007/3-540-60630-0_4

M3 - Paper

SP - 72

EP - 88

ER -

Brinksma H, (ed.), Mader AH, Cleaveland WR, (ed.), Larsen KG, (ed.), Larsen KG, (ed.), Margaria T, (ed.) et al. Modal µ-Calculus, Model Checking and Gauß Elimination. 1995. Paper presented at First International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995, Aarhus, Denmark. https://doi.org/10.1007/3-540-60630-0_4