Advertisement

SAT-Based (Parametric) Reachability for a Class of Distributed Time Petri Nets

  • Wojciech Penczek
  • Agata Pòłrola
  • Andrzej Zbrzezny
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6550)

Abstract

Formal methods - among them the model checking techniques - play an important role in the design and production of both systems and software. In this paper we deal with an adaptation of the bounded model checking methods for timed systems, developed for timed automata, to the case of time Petri nets. We consider distributed time Petri nets and parametric reachability checking, but the approach can be easily adapted to verification of other kinds of properties for which the bounded model checking methods exist. A theoretical description is supported by some experimental results, generated using an extension of the model checker verICS.

Keywords

Model Check Mutual Exclusion Propositional Variable Propositional Formula Concrete State 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.: Model checking for real-time systems. In: Proc. of the 5th Symp. on Logic in Computer Science (LICS 1990), pp. 414–425. IEEE Computer Society Press, Los Alamitos (1990)Google Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS 1992), pp. 157–166. IEEE Computer Society Press, Los Alamitos (1992)Google Scholar
  3. 3.
    Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 243–259. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    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
  5. 5.
    Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. on Software Eng. 17(3), 259–273 (1991)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: Proc. of the 9th IFIP World Computer Congress. Information Processing, vol. 9, pp. 41–46. North Holland/IFIP (September 1983)Google Scholar
  7. 7.
    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
  8. 8.
    Boucheneb, H., Barkaoui, K.: Relevant timed schedules / clock valuations for constructing time petri net reachability graphs. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 265–279. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Boucheneb, H., Berthelot, G.: Towards a simplified building of time Petri nets reachability graph. In: Proc. of the 5th Int. Workshop on Petri Nets and Performance Models, pp. 46–55 (October 1993)Google Scholar
  10. 10.
    Bucci, G., Fedeli, A., Sassoli, L., Vicaro, E.: Modeling flexible real time systems with preemptive time Petri nets. In: Proc. of the 15th Euromicro Conference on Real-Time Systems (ECRTS 2003), pp. 279–286. IEEE Computer Society Press, Los Alamitos (2003)CrossRefGoogle Scholar
  11. 11.
    Bucci, G., Vicaro, E.: Compositional validation of time-critical systems using communicating time Petri nets. IEEE Trans. on Software Eng. 21(12), 969–992 (1995)CrossRefGoogle Scholar
  12. 12.
    Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)CrossRefzbMATHGoogle Scholar
  13. 13.
    Dembinski, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B.z., Zbrzezny, A.: VerICS: A tool for verifying timed automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 278–283. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. 14.
    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
  15. 15.
    Gardey, G., Roux, O.H., Roux, O.F.: Using zone graph method for computing the state space of a time Petri net. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 246–259. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. 16.
    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
  17. 17.
    Huhn, M., Niebert, P., Wallner, F.: Verification based on local states. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 36–51. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  18. 18.
    Janicki, R.: Nets, sequential components and concurrency relations. Theoretical Computer Science 29, 87–121 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Lilius, J.: Efficient state space search for time Petri nets. In: Proc. of MFCS Workshop on Concurrency, Brno 1998. ENTCS, vol. 18. Elsevier, Amsterdam (1999)Google Scholar
  20. 20.
    Mascarenhas, R., Karumuri, D., Buy, U., Kenyon, R.: Modeling and analysis of a virtual reality system with time Petri nets. In: Proc. of the 20th Int. Conf. on Software Engineering (ICSE 1998), pp. 33–42. IEEE Computer Society Press, Los Alamitos (1998)CrossRefGoogle Scholar
  21. 21.
    Merlin, P., Farber, D.J.: Recoverability of communication protocols – implication of a theoretical study. IEEE Trans. on Communications 24(9), 1036–1043 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Okawa, Y., Yoneda, T.: Symbolic CTL model checking of time Petri nets. Electronics and Communications in Japan, Scripta Technica 80(4), 11–20 (1997)CrossRefGoogle Scholar
  23. 23.
    Penczek, W., Półrola, A.: Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 37–76. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  24. 24.
    Penczek, W., Półrola, A., Woźna, B., Zbrzezny, A.: Bounded model checking for reachability testing in time Petri nets. In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2004). Informatik-Berichte, vol. 170(1), pp. 124–135. Humboldt University (2004)Google Scholar
  25. 25.
    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
  26. 26.
    Penczek, W., Woźna, B., Zbrzezny, A.: Branching time bounded model checking for elementary net systems. Technical Report 940, ICS PAS, Ordona 21, 01-237 Warsaw (January 2002)Google Scholar
  27. 27.
    Penczek, W., Woźna, B., Zbrzezny, A.: Towards bounded model checking for the universal fragment of TCTL. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 265–288. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  28. 28.
    Półrola, A., Penczek, W.: Minimization algorithms for time Petri nets. Fundamenta Informaticae 60(1-4), 307–331 (2004)MathSciNetzbMATHGoogle Scholar
  29. 29.
    Popova, L.: On time Petri nets. Elektronische Informationsverarbeitung und Kybernetik 27(4), 227–244 (1991)zbMATHGoogle Scholar
  30. 30.
    Popova-Zeugmann, L., Schlatter, D.: Analyzing paths in time Petri nets. Fundamenta Informaticae 37(3), 311–327 (1999)MathSciNetzbMATHGoogle Scholar
  31. 31.
    Romeo: A tool for time Petri net analysis (2000), http://www.irccyn.ecnantes.fr/irccyn/d/en/equipes/TempsReel/logs
  32. 32.
    Strichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480–494. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  33. 33.
    Traonouez, L.-M., Lime, D., Roux, O.H.: Parametric model-checking of time petri nets with stopwatches using the state-class graph. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 280–294. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  34. 34.
    Virbitskaite, I.B., Pokozy, E.A.: A partial order method for the verification of time petri nets. In: Ciobanu, G., Păun, G. (eds.) FCT 1999. LNCS, vol. 1684, pp. 547–558. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  35. 35.
    Woźna, B.: ACTL* properties and bounded model checking. Fundamenta Informaticae 63(1), 65–87 (2004)MathSciNetzbMATHGoogle Scholar
  36. 36.
    Woźna, B., Zbrzezny, A., Penczek, W.: Checking reachability properties for timed automata via SAT. Fundamenta Informaticae 55(2), 223–241 (2003)MathSciNetzbMATHGoogle Scholar
  37. 37.
    Yovine, S.: Model checking timed automata. In: Rozenberg, G. (ed.) EEF School 1996. LNCS, vol. 1494, pp. 114–152. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  38. 38.
    Zbrzezny, A.: Improvements in SAT-based reachability analysis for timed automata. Fundamenta Informaticae 60(1-4), 417–434 (2004)MathSciNetzbMATHGoogle Scholar
  39. 39.
    Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae 67(1-3), 303–322 (2005)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Wojciech Penczek
    • 1
    • 2
  • Agata Pòłrola
    • 3
  • Andrzej Zbrzezny
    • 4
  1. 1.ICSPolish Academy of SciencesWarsawPoland
  2. 2.ICSUniversity of PodlasieSiedlcePoland
  3. 3.FMCSUniversity of ŁódźŁódźPoland
  4. 4.IMCSJan Długosz UniversityCzȩstochowaPoland

Personalised recommendations