An approach to effective model-checking of real-time Finite-State Machines in mu-calculus | SpringerLink
Skip to main content
Springer Nature Link
Log in

An approach to effective model-checking of real-time Finite-State Machines in mu-calculus

An extended abstract

  • Conference paper
  • First Online:
Logical Foundations of Computer Science (LFCS 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 813))

Included in the following conference series:

Abstract

The paper presents two main results. The first one is a polynomial Model-Checker (PMC) for a new representative subclass of formulae of the propositional mu-calculus. Formulae in this class have some discipline of alternation of fixed points. The other result extends the model checking techniques to the so-called semilinear class of finite Kripke structures induced by Finite-State Machines with multiple clock functioning in real time.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. R.S. Streett, E.A.Emerson. An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus // Information and Control, v.81, n.3, 1989 // pp. 249–264.

    Google Scholar 

  2. S.A. Berezin, N.V. Shilov, V.P. Shneider. An effective model checking for Mu-calculus: from finite systems towards systems with real time // Bulletin of the Novosibirsk Computer Center, Series: Computer Science, No. 1, 1993// pp. 73–86.

    Google Scholar 

  3. R. Cleaveland, M. Dreimueller and B. Steffen. Faster Model-Checker for the Modal Mu-Calculus // proc. of TAV-91, Montreal // pp. 383–400.

    Google Scholar 

  4. E.A. Emerson, C.S. Julta, A.P. Sistla. On model-checking for fragments of Mucalculus // Proc. of ”Computer Aided Verification CAV-93”, Lect. Notes in Comp. Sci., 1993// pp. 385–396

    Google Scholar 

  5. N.V. Shilov. Propositional Dynamic Logic with Fixed Points: Algoritmic Tools for verification of Finite State Machines // Proc. of ”Logic Foundations of Comp. Sci. — Tver'92”. Lect. Notes in Comp. Sci., volo. 620, 1992// pp.452–458.

    Google Scholar 

  6. J.S. Ostroff. Automated Verificaion of Timed Transition Models. //Lect. Notes Comput. Sci., Vol 407 // pp. 247–256.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Novosibirsk State University, Pirogova st., 2, 630090, Novosibirsk, Russia

    S. A. Berezin

  2. Institute of Informatics Systems Siberian Division of Russian Academy of Science, Lavrentjev av., 6, 630090, Novosibirsk, Russia

    N. V. Shilov

Authors
  1. S. A. Berezin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. N. V. Shilov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Anil Nerode Yu. V. Matiyasevich

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Berezin, S.A., Shilov, N.V. (1994). An approach to effective model-checking of real-time Finite-State Machines in mu-calculus. In: Nerode, A., Matiyasevich, Y.V. (eds) Logical Foundations of Computer Science. LFCS 1994. Lecture Notes in Computer Science, vol 813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58140-5_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-58140-5_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58140-6

  • Online ISBN: 978-3-540-48442-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation