Bounded Parametric Model Checking for Elementary Net Systems

  • Michał Knapik
  • Maciej Szreter
  • Wojciech Penczek
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6550)


Bounded Model Checking (BMC) is an efficient verification method for reactive systems. BMC has been applied so far to verification of properties expressed in (timed) modal logics, but never to their parametric extensions. In this paper we show, for the first time that BMC can be extended to PRTECTL – a parametric extension of the existential version of CTL. To this aim we define a bounded semantics and a translation from PRTECTL to SAT. The implementation of the algorithm for Elementary Net Systems is presented, together with some experimental results.


Model Check Inductive Assumption Mutual Exclusion Propositional Formula Kripke Structure 
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.
    Alur, R., Henzinger, T., Vardi, M.: Parametric real-time reasoning. In: Proc. of the 25th Ann. Symp. on Theory of Computing (STOC 1993), pp. 592–601. ACM, New York (1993)Google Scholar
  2. 2.
    Benedetti, M., Cimatti, A.: Bounded model checking for past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 18–33. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. of the ACM/IEEE Design Automation Conference (DAC 1999), pp. 317–320 (1999)Google Scholar
  4. 4.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. 5.
    Bruyére, V., Dall’Olio, E., Raskin, J.-F.: Durations and parametric model-checking in timed automata. ACM Transactions on Computational Logic 9(2), 1–21 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Emerson, E.A., Trefler, R.: Parametric quantitative temporal reasoning. In: Proc. of the 14th Symp. on Logic in Computer Science (LICS 1999), pp. 336–343. IEEE Computer Society Press, Los Alamitos (July 1999)Google Scholar
  7. 7.
    Heljanko, K.: Bounded reachability checking with process semantics. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 218–232. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  8. 8.
    Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 189–203. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
  10. 10.
    Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 9409–9423. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  11. 11.
    Penczek, W., Woźna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae 51(1-2), 135–156 (2002)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Bruyère, V., Raskin, J.-F.: Real-time model-checking: Parameters everywhere. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 100–111. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Woźna, B.: ACTL* properties and bounded model checking. In: Czaja, L. (ed.) Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2003), vol. 2, pp. 591–605. Warsaw University (2003)Google Scholar
  14. 14.
    Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae 85(1-4), 513–531 (2008)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Michał Knapik
    • 1
  • Maciej Szreter
    • 1
  • Wojciech Penczek
    • 1
    • 2
  1. 1.Institute of Computer SciencePASWarszawaPoland
  2. 2.Institute of InformaticsPodlasie AcademySiedlcePoland

Personalised recommendations