A linear algorithm for solving fixed-point equations on transition systems

  • Bart Vergauwen
  • Johan Lewi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)


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].


model checking modal logics transition systems 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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
  2. [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
  3. [C]
    Cleaveland, R.: Tableau-based model checking in the propositional μcalculus, Acta Informatica, 1990Google Scholar
  4. [CS]
    Cleaveland, R., Steffen, B.: Computing Behavioural Relations, Logically, ICALP 91, pp. 127–138, LNCS 510Google Scholar
  5. [D]
    Dicky, A.: An algebraic and algorithmic method of analysing transition systems, TCS, 46, 285–303, 1986Google Scholar
  6. [EL]
    Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional μ-calculus, LICS, 267–278, 1986Google Scholar
  7. [K]
    Kozen, D.: Results on the propositional μ-calculus, TCS, 27, 333–354, 1983Google Scholar
  8. [SW]
    Stirling, C., Walker, D.: Local model checking in the modal mu-calculus, CAAP 1989, pp. 369–383, LNCS 351Google Scholar
  9. [T]
    Tarski, A.: A lattice-theoretic fixpoint theorem and its applications, Pacific Journal of Mathematics, vol 5, 1955Google Scholar
  10. [W]
    Winskel, G.: On the compositional checking of validity, LNCS 458, 481–501, CONCUR'90Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Bart Vergauwen
    • 1
  • Johan Lewi
    • 1
  1. 1.Department of Computer ScienceKU LeuvenLeuvenBelgium

Personalised recommendations