Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Automated Analysis of Asynchronously Communicating Systems Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization

Authors : Peter Gjøl Jensen, Kim Guldstrand Larsen, Jiří Srba

Published in: Model Checking Software

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Automatic strategy synthesis for a given control objective can be used to generate correct-by-construction controllers of reactive systems. The existing symbolic approach for continuous timed games is a computationally hard task and current tools like UPPAAL TiGa often scale poorly with the model complexity. We suggest an explicit approach for strategy synthesis in the discrete-time setting and show that even for systems with closed guards, the existence of a safety discrete-time strategy does not imply the existence of a safety continuous-time strategy and vice versa. Nevertheless, we prove that the answers to the existence of discrete-time and continuous-time safety strategies coincide on a practically motivated subclass of urgent controllers that either react immediately after receiving an environmental input or wait with the decision until a next event is triggered by the environment. We then develop an on-the-fly synthesis algorithm for discrete timed-arc Petri net games. The algorithm is implemented in our tool TAPAAL and based on the experimental evidence, we discuss the advantages of our approach compared to the symbolic continuous-time techniques.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Certification for -Calculus with Winning Strategies
next chapter Finite-Horizon Bisimulation Minimisation for Probabilistic Systems
Footnotes
1
UPPAAL TiGa only exists in a 32 bit version, but for none of the tests the 4 GB limit was exceeded for UPPAAL TiGa.
 
Literature
1.
2.
3.
Andersen, M., Larsen, H.G., Srba, J., Sørensen, M.G., Haahr Taankvist, J.: Verification of liveness properties on closed timed-arc Petri nets. In: Kučera, A., Henzinger, T.A., Nešetřil, J., Vojnar, T., Antoš, D. (eds.) MEMICS 2012. LNCS, vol. 7721, pp. 69–81. Springer, Heidelberg (2013)CrossRef
4.
Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-TiGa: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007)CrossRef
5.
Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Third International Conference on Quantitative Evaluation of Systems, pp. 125–126 (2006)
6.
Berthomieu, B., Vernadat, F.: Time Petri nets analysis with TINA. In: Third International Conference on Quantitative Evaluation of Systems, pp. 123–124. IEEE Computer Society (2006)
7.
Birch, S.V., Jacobsen, T.S., Jensen, J.J., Moesgaard, C., Nørgaard Samuelsen, N., Srba, J.: Interval abstraction refinement for model checking of timed-arc Petri nets. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 237–251. Springer, Heidelberg (2014)
8.
Bolognesi, T., Lucidi, F., Trigila, S.: From timed Petri nets to timed LOTOS. In: Proceedings of the IFIP WG6.1 Tenth International Symposium on Protocol Specification, Testing and Verification X, North-Holland, pp. 395–408 (1990)
9.
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)CrossRef
10.
Bozga, M., Maler, O., Tripakis, S.: Efficient verification of timed automata using dense and discrete time semantics. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 125–141. Springer, Heidelberg (1999)CrossRef
11.
Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005)CrossRef
12.
Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. J. Symbolic Logic 28(4), 289–290 (1963)MathSciNetCrossRef
13.
Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians (Stockholm, 1962), pp. 23–35. Institute Mittag-Leffler (1963)
14.
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, Third Edition, 3rd edn. The MIT Press (2009). ISBN: 0262033844 9780262033848
15.
David, A., Jacobsen, L., Jacobsen, M., Jørgensen, K.Y., Møller, M.H., Srba, J.: TAPAAL 2.0: integrated development environment for timed-arc Petri nets. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492–497. Springer, Heidelberg (2012)CrossRef
16.
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)CrossRef
17.
Finkbeiner, B.: Bounded synthesis for Petri games. In: Meyer, R., et al. (eds.) Olderog-Festschrift. LNCS, vol. 9360, pp. 223–237. Springer, Heidelberg (2015)CrossRef
18.
Finkbeiner, B., Olderog, E.: Petri games: synthesis of distributed systems with causal memory. In: Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, vol. 161 of EPTCS, pp. 217–230 (2014)
19.
Finkbeiner, B., Peter, H.-J.: Template-based controller synthesis for timed systems. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 392–406. Springer, Heidelberg (2012)CrossRef
20.
Gale, D., Stewart, F.M.: Infinite games with perfect information. In: Contributions to the Theory of Games. Annals of Mathematics Studies, no. 28, vol. 2, pp. 245–266. Princeton University Press, Princeton, N.J (1953)
21.
Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Romeo: a tool for analyzing time Petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005)CrossRef
22.
Gurevich, Y.: Games people play. In: Lane, S.M., Siefkes, D. (eds.) The Collected Works of J. Richard Büchi, pp. 517–524. Springer, Berlin (1990)
23.
Hanisch, H.-M.: Analysis of place/transition nets with timed arcs and its application to batch process control. In: Marsan, M.A. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 282–299. Springer, Heidelberg (1993)CrossRef
24.
Jensen, P.G., Larsen, K.G., Srba, J., Sørensen, M.G., Taankvist, J.H.: Memory efficient data structures for explicit verification of timed systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 307–312. Springer, Heidelberg (2014)CrossRef
25.
Jørgensen, K.Y., Larsen, K.G., Srba, J.: Time-darts: a data structure for verification of closed timed automata. In: Proceedings Seventh Conference on Systems Software Verification, vol. 102 of EPTCS, pp. 141–155. Open Publishing Association (2012)
26.
Kempf, J.-F., Bozga, M., Maler, O.: As soon as probable: optimal scheduling under stochastic uncertainty. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 385–400. Springer, Heidelberg (2013)CrossRef
27.
Larsen, K.G., Wang, Y.: Time-abstracted bisimulation: implicit specifications and decidability. Inf. Comput. 134(2), 75–101 (1997)MathSciNetCrossRefMATH
28.
Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points (extended abstract). In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 53–66. Springer, Heidelberg (1998)CrossRef
29.
Maler, O., Larsen, K.G., Krogh, B.H.: On zone-based analysis of duration probabilistic automata. In: Proceedings 12th International Workshop on Verification of Infinite-State Systems, vol.39 of EPTCS, pp. 33–46 (2010)
30.
Mateo, J.A., Srba, J., Sørensen, M.G.: Soundness of timed-arc workflow nets in discrete and continuous-time semantics. Fundamenta Informaticase 140(1), 89–121 (2015)MathSciNetCrossRef
31.
Peter, H.: Component-based abstraction refinement for timed controller synthesis. In: IEEE, pp. 364–374. IEEE Computer Society (2009)
32.
Peter, H.-J., Ehlers, R., Mattmüller, R.: Synthia: verification and synthesis for timed automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 649–655. Springer, Heidelberg (2011)CrossRef
33.
Pnueli, A., Asarin, E., Maler, O., Sifakis, J.: Controller synthesis for timed automata. System Structure and Control. Citeseer, Elsevier (1998)
34.
Raskin, J.F., Samuelides, M., Begin, L.V.: Petri games are monotone but difficult to decide. Technical report, Université Libre De Bruxelles (2003)
35.
Ruiz, V.V., Cuartero Gomez, F., de Frutos Escrig, D.: On non-decidability of reachability for timed-arc Petri nets. In: Proceedings of the 8th International Workshop on Petri Nets and Performance Models, pp. 188–196 (1999)
36.
Zhou, Q., Wang, M., Dutta, S.P.: Generation of optimal control policy for flexible manufacturing cells: a Petri net approach. Int. J. Adv. Manuf. Technol. 10(1), 59–65 (1995)CrossRef
Metadata
Title
Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization
Authors
Peter Gjøl Jensen
Kim Guldstrand Larsen
Jiří Srba
Copyright Year
2016
Book
Model Checking Software

Print ISBN: 978-3-319-32581-1

Electronic ISBN: 978-3-319-32582-8

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-32582-8_9

Premium Partner

    Image Credits