Model Checking for Multi-valued Computation Tree Logics

  • Beata Konikowska
  • Wojciech Penczek
Part of the Studies in Fuzziness and Soft Computing book series (STUDFUZZ, volume 114)


A multi-valued version of CTL* (mv-CTL*), where both the propositions and the accessibility relation are multi-valued taking values in a finite quasi-Boolean algebra, is defined. A translation from my-CTL* model checking to CTL* model checking is investigated. First, the case where the elements of quasi-Boolean algebras are totally ordered is considered. Secondly, it is shown how to design a translation algorithm for the two most commonly applied quasi-Boolean algebras. This construction suggests the way one can deal with more complex quasi-Boolean algebras if necessary.


Model Check Modal Logic Temporal Logic Propositional Variable State Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Biere, A., Cimatti, A., Clarke, E., Fujita, M. and Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs, Proc. of ACM/IEEE Design Automation Conference (DAC’99) (1999) 317–320Google Scholar
  2. 2.
    Biere, A., Cimatti, A., Clarke, E. and Zhu, Y.: Symbolic model checking without BDDs, Proc. of TACAS’99, LNCS, vol. 1579, Springer-Verlag (1999) 193–207Google Scholar
  3. 3.
    Bruns, G. and Godefroid, P.: Model checking partial state spaces, Proc. of CAV’99, LNCS, vol. 1633, Springer-Verlag (1999) 274–287Google Scholar
  4. 4.
    Bruns, G. and Godefroid, P.: Generalized model checking: reasoning about partial state spaces, Proc. of CONCUR’00, LNCS, vol. 1877, Springer-Verlag, (2000) 168–182Google Scholar
  5. 5.
    Bryant, R.: Graph-based algorithms for boolean function manipulation, IEEE Transaction on Computers 35, (8) (1986) 677–691MATHCrossRefGoogle Scholar
  6. 6.
    Bryant, R.: Binary Decision Diagrams and beyond: Enabling technologies for formal verification, Proc. of Int. Conf. on Computer-Aided Design (ICCAD’95) (1995) 236–243Google Scholar
  7. 7.
    Bernholtz, O., Vardi, M.Y. and Wolper, P.: An automata-theoretic approach to branching-time model checking, Proc. of CAV’94, LNCS, vol. 818, Springer-Verlag (1994) 142–155Google Scholar
  8. 8.
    Chechik, M., Devereux, B. and Easterbrook, S.: Implementing a multi-valued symbolic model-checker, Proc. of TACAS’01, LNCS, vol. 2031, Springer-Verlag (2001) 404–419Google Scholar
  9. 9.
    Chechik, M., Devereux, B., Easterbrook, S., Lai, A.Y.C. and Petrovykh, V.: Efficient multiple-valued model-checking using lattice representations, Proc. of CONCUR’01, LNCS, vol. 2154, Springer-Verlag (2001) 441–455Google Scholar
  10. 10.
    Chechik, M., Devereux, B. and Gurfinkel, A.: Model checking infinite state-spaces systems with fine-grained abstractions using spin, Proc. of SPIN’01, LNCS, vol. 2057, Springer-Verlag (2001) 16–36Google Scholar
  11. 11.
    Chechik, M., Easterbrook, S. and Petrovykh, V.: Model checking over multi-valued temporal logics, Proc. of FME’01, LNCS, vol. 2001, Springer-Verlag (2001) 72–98Google Scholar
  12. 12.
    Clarke, E.M., Emerson, E.A. and Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach, ACM Transactions on Programming Languages and Systems 8, (2) (1986) 244–263MATHCrossRefGoogle Scholar
  13. 13.
    Clarke, E.M., Grumberg, O. and Peled, D.: Model Checking, MIT Press (1999)Google Scholar
  14. 14.
    Chechik, M.: On interpreting results of model-checking with abstraction, Tech. Report 417, University of Toronto (2000)Google Scholar
  15. 15.
    Dams, D., Gerth, R., Dohmen, G., Herrmann, R., Kelb, P. and Pargmann, H.: Model checking using adaptive state and data abstraction, Proc. of CAV’94, LNCS, vol. 818, Springer-Verlag (1994) 455–467Google Scholar
  16. 16.
    Dams, D., Grumberg, O. and Gerth, R.: Abstract interpretation of reactive systems: Abstractions preserving ACTL*, ECTL* and CTL*, Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET’94), Elsevier Science Publishers (1994)Google Scholar
  17. 17.
    Easterbrook, S. and Chechik, M.: A framework for multi-valued reasoning over inconsistent viewpoints, Proc. of ICSE’01 (2001) 411–420Google Scholar
  18. 18.
    Emerson, E.A.: Handbook of Theoretical Computer Science, vol. B: Formal Methods and Semantics, ch. Temporal and Modal Logic, Elsevier (1990) 9951067Google Scholar
  19. 19.
    Emerson, E.A. and Sistla, A.P.: Symmetry and model checking, Formal Methods in System Design 9 (1995) 105–131CrossRefGoogle Scholar
  20. 20.
    Fitting, M.: Many-valued modal logics, Fundamenta Informaticae 15, (3–4) (1991) 335–350MathSciNetGoogle Scholar
  21. 21.
    Fitting, M.: Many-valued modal logics II, Fundamenta Informaticae 17 (1992) 55–73MathSciNetMATHGoogle Scholar
  22. 22.
    Hazelhurst, S.: Compositional model checking of partially ordered state spaces, Ph.D. thesis, University of British Columbia (1996)Google Scholar
  23. 23.
    Lichtenstein, O. and Pnueli, A.: Checking that finite-state concurrent programs satisfy their linear specification, Proc. of the 12th ACM Symposium on Principles of Programming Languages (POPL’84), ACM Press (1984) 97–107Google Scholar
  24. 24.
    Peled, D.: Partial order reduction: Linear and branching temporal logics and process algebras, Proc. of Partial Order Methods in Verification (POMIV’96), ACM/AMS DIMACS Series, vol. 29, Amer. Math. Soc. (1996) 79–88Google Scholar
  25. 25.
    Penczek, W., Szreter, M., Gerth, R. and Kuiper, R.: Improving partial order reductions for universal branching time properties, Fundamenta Informaticae 43 (2000) 245–267MathSciNetMATHGoogle Scholar
  26. 26.
    Penczek, W. and Wozna, B.: Towards bounded model checking for Timed Automata, Proc. of the Int. Workshop on Concurrency Specification and Programming (CSandP’01) (2001) 195–209Google Scholar
  27. 27.
    Valmari, A.: Stubborn sets for reduced state space generation, Proc. of the Int. Conf. on Applications and Theory of Petri Nets (ICATPN’89), LNCS, vol. 483, Springer-Verlag (1989) 491–515Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Beata Konikowska
    • 1
  • Wojciech Penczek
    • 1
    • 2
  1. 1.PASInstitute of Computer ScienceWarsawPoland
  2. 2.Akademia PodlaskaInstitute of InformaticsSiedlcePoland

Personalised recommendations