A linear algorithm for solving fixed-point equations on transition systems
In this paper we present an algorithm for effectively computing extremal fixed-points of a system of mutually recursive equations over a finite transition system. The proposed algorithm runs in time linear in the size of the transition system and linear in the size of the system of equations, thereby improving on [AC].
Keywordsmodel checking modal logics transition systems
Unable to display preview. Download preview PDF.
- [AC]Arnold, A., Crubille, P.: A linear algorithm to solve fixed-points equations on transition systems, Information Processing Letters, vol.29, 57–66, 1988Google Scholar
- [CES]Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Progr. Languages and Systems, Vol.8, No. 2, pp. 244–263, April 1986Google Scholar
- [C]Cleaveland, R.: Tableau-based model checking in the propositional μcalculus, Acta Informatica, 1990Google Scholar
- [CS]Cleaveland, R., Steffen, B.: Computing Behavioural Relations, Logically, ICALP 91, pp. 127–138, LNCS 510Google Scholar
- [D]Dicky, A.: An algebraic and algorithmic method of analysing transition systems, TCS, 46, 285–303, 1986Google Scholar
- [EL]Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional μ-calculus, LICS, 267–278, 1986Google Scholar
- [K]Kozen, D.: Results on the propositional μ-calculus, TCS, 27, 333–354, 1983Google Scholar
- [SW]Stirling, C., Walker, D.: Local model checking in the modal mu-calculus, CAAP 1989, pp. 369–383, LNCS 351Google Scholar
- [T]Tarski, A.: A lattice-theoretic fixpoint theorem and its applications, Pacific Journal of Mathematics, vol 5, 1955Google Scholar
- [W]Winskel, G.: On the compositional checking of validity, LNCS 458, 481–501, CONCUR'90Google Scholar