×

Reachability analysis for timed automata using max-plus algebra. (English) Zbl 1279.68214

Summary: We show that max-plus polyhedra are usable as a data structure in reachability analysis of timed automata. Drawing inspiration from the extensive work that has been done on difference bound matrices, as well as previous work on max-plus polyhedra in other areas, we develop the algorithms needed to perform forward and backward reachability analysis using max-plus polyhedra. To show that the approach works in practice and theory alike, we have created a proof-of-concept implementation on top of the model checker opaal.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
15A80 Max-plus and related algebras
68P05 Data structures
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aceto, Luca; Ingólfsdóttir, Anna; Larsen, Kim Guldstrand; Srba, Jiřı´, Reactive Systems (2007), Cambridge University Press · Zbl 1141.68043
[2] Allamigeon, Xavier; Gaubert, Stéphane; Goubault, Éric, Inferring min and max invariants using max-plus polyhedra, (Alpuente, Marı´a; Vidal, Germán, SAS, Lecture Notes in Computer Science, vol. 5079 (2008), Springer), 189-204 · Zbl 1149.68346
[3] Xavier Allamigeon, Stéphane Gaubert, Éric Goubault, Computing the extreme points of tropical polyhedra, 2009. arXiv:0904.3436; Xavier Allamigeon, Stéphane Gaubert, Éric Goubault, Computing the extreme points of tropical polyhedra, 2009. arXiv:0904.3436
[4] Allamigeon, Xavier; Gaubert, Stéphane; Goubault, Éric, The tropical double description method, (Marion, Jean-Yves; Schwentick, Thomas, STACS, LIPIcs, vol. 5 (2010), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 47-58 · Zbl 1230.52024
[5] Rajeev Alur, Costas Courcoubetis, David L. Dill, Nicolas Halbwachs, Howard Wong-Toi, An implementation of three algorithms for timing verification based on automata emptiness, in: IEEE Real-Time Systems Symposium, 1992, pp. 157-166.; Rajeev Alur, Costas Courcoubetis, David L. Dill, Nicolas Halbwachs, Howard Wong-Toi, An implementation of three algorithms for timing verification based on automata emptiness, in: IEEE Real-Time Systems Symposium, 1992, pp. 157-166.
[6] Alur, Rajeev; Dill, DavidL., Automata for modeling real-time systems, (Paterson, Mike, ICALP, Lecture Notes in Computer Science, vol. 443 (1990), Springer), 322-335 · Zbl 0765.68150
[7] Alur, Rajeev; Dill, David L., A theory of timed automata, Theoret. Comput. Sci., 126, 2, 183-235 (1994) · Zbl 0803.68071
[8] Asarin, Eugene; Bozga, Marius; Kerbrat, Alain; Maler, Oded; Pnueli, Amir; Rasse, Anne, Data-structures for the verification of timed automata, (Maler, Oded, Hybrid and Real-Time Systems, Lecture Notes in Computer Science, vol. 1201 (1997), Springer: Springer Berlin/Heidelberg), 346-360
[9] Bagnara, Roberto; Ricci, Elisa; Zaffanella, Enea; Hill, Patricia M., Possibly not closed convex polyhedra and the parma polyhedra library, (Proceedings of the 9th International Symposium on Static Analysis, Lecture Notes in Computer Science, vol. 2477 (2002), Springer-Verlag), 213-229 · Zbl 1015.68215
[10] Behrmann, Gerd; Bouyer, Patricia; Larsen, Kim G.; Pelánek, Radek, Lower and upper bounds in zone-based abstractions of timed automata, Int. J. Softw. Tools Technol. Transfer, 8, 204-215 (2006) · Zbl 1126.68453
[11] Behrmann, Gerd; Larsen, Kim G.; Pearson, Justin; Weise, Carsten; Yi, Wang, Efficient timed reachability analysis using clock difference diagrams, (Halbwachs, Nicolas; Peled, Doron, Proc. CAV’99, Lecture Notes in Computer Science, vol. 1633 (1999), Springer), 682
[12] Johan Bengtsson, Clocks, DBMs, and States in Timed Systems, Ph.D. thesis, Uppsala University, June 2002.; Johan Bengtsson, Clocks, DBMs, and States in Timed Systems, Ph.D. thesis, Uppsala University, June 2002.
[13] Bouyer, Patricia; Laroussinie, François; Reynier, Pierre-Alain, Diagonal constraints in timed automata: forward analysis of timed systems, (Proc. FORMATS’05, LNCS, vol. 3829 (2005), Springer), 112-126 · Zbl 1175.68256
[14] Bozga, Marius; Maler, Oded; Pnueli, Amir; Yovine, Sergio, Some progress in the symbolic verification of timed automata, (Lecture Notes in Computer Science (1997), Springer-Verlag), 179-190
[15] Butkovič, Peter; Schneider, Hans; Sergeev, Sergeı˘, Generators, extremals and bases of max cones, Linear Algebra Appl., 421, 2-3, 394-406 (2007) · Zbl 1119.15018
[16] Cousot, Patrick; Halbwachs, Nicolas, Automatic discovery of linear restraints among variables of a program, (POPL ’78: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (1978), ACM Press), 84-96
[17] Dill, David L., Timing assumptions and verification of finite-state concurrent systems, (Sifakis, Joseph., Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, vol. 407 (1989), Springer), 197-212
[18] Jesper Dyhrberg, Qi Lu, Michael Madsen, Søren Ravn, Computations on zones using max-plus algebra, Bachelor’s project, Aalborg University, 2010. Available from: <https://services.cs.aau.dk/public/tools/library/details.php?id=1274952619>; Jesper Dyhrberg, Qi Lu, Michael Madsen, Søren Ravn, Computations on zones using max-plus algebra, Bachelor’s project, Aalborg University, 2010. Available from: <https://services.cs.aau.dk/public/tools/library/details.php?id=1274952619>
[19] Rüdiger Ehlers, Daniel Fass, Michael Gerke, Hans-Jörg Peter, Fully symbolic timed model checking using constraint matrix diagrams, in: Real-Time Systems Symposium, IEEE International, 2010, pp. 360-371.; Rüdiger Ehlers, Daniel Fass, Michael Gerke, Hans-Jörg Peter, Fully symbolic timed model checking using constraint matrix diagrams, in: Real-Time Systems Symposium, IEEE International, 2010, pp. 360-371.
[20] Fahrenberg, Uli; Larsen, Kim G.; Thrane, Claus, Verification, performance analysis and controller synthesis for real-time systems, (Broy, Manfred; Sitou, Wassiou; Hoare, Tony, Engineering Methods and Tools for Software Safety and Security, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 22 (2009), IOS Press) · Zbl 1274.68185
[21] Floyd, Robert W., Algorithm 97: shortest path, Commun. ACM, 5, 345 (1962)
[22] Gaubert, Stéphane; Katz, Ricardo D., The Minkowski theorem for max-plus convex sets, Linear Algebra Appl., 421, 2-3, 356-369 (2007) · Zbl 1110.52002
[23] Giacobazzi, Roberto; Ranzato, Francesco, Compositional optimization of disjunctive abstract interpretations, (Proc. of the 1996 European Symposium on Programming, Lecture Notes in Computer Science, vol. 1058 (1996), Springer-Verlag), 141-155 · Zbl 1360.68363
[24] Henzinger, Thomas A.; Nicollin, Xavier; Sifakis, Joseph; Yovine, Sergio, Symbolic model checking for real-time systems, Inf. Comput., 111, 2, 193-244 (1994) · Zbl 0806.68080
[25] Larsen, Kim G.; Pearson, Justin; Weise, Carsten; Yi, Wang, Clock difference diagrams, Nordic J. Comput., 6, 271-298 (1999) · Zbl 0937.68086
[26] Qi Lu, Michael Madsen, Martin Milata, Søren Ravn, Computations on zones using max-plus algebra, Project report, Aalborg University, January 2011. Available from: http://download.birdiesoft.dk/maxplus.pdf; Qi Lu, Michael Madsen, Martin Milata, Søren Ravn, Computations on zones using max-plus algebra, Project report, Aalborg University, January 2011. Available from: http://download.birdiesoft.dk/maxplus.pdf · Zbl 1279.68214
[27] Miné, Antoine, A new numerical abstract domain based on difference-bound matrices, (Proceedings of the 2nd Symposium on Programs as Data Objects (PADO 2001), Lecture Notes in Computer Science, vol. 2053 (2001), Springer-Verlag), 155-172 · Zbl 0984.68034
[28] Miné, Antoine, The octagon abstract domain, (AST 2001 in WCRE 2001, IEEE (2001), IEEE CS Press), 310-319 · Zbl 1105.68069
[29] Møller, Jesper B.; Lichtenberg, Jakob; Andersen, HenrikReif; Hulgaard, Henrik, Difference decision diagrams, (Flum, Jörg; Rodríguez-Artalejo, Mario, CSL, Lecture Notes in Computer Science, vol. 1683 (1999), Springer), 111-125 · Zbl 0944.68040
[30] Mads Chr.Olesen, Kenneth Y. JÃrgensen, <http://www.opaal-modelchecker.com/>; Mads Chr.Olesen, Kenneth Y. JÃrgensen, <http://www.opaal-modelchecker.com/>
[31] Sankaranarayanan, Sriram; Ivancic, Franjo; Shlyakhter, Ilya; Gupta, Aarti, Static analysis in disjunctive numerical domains, (Yi, Kwangkeun, Static Analysis, Lecture Notes in Computer Science, vol. 4134 (2006), Springer: Springer Berlin/Heidelberg), 3-17 · Zbl 1225.68077
[32] Uppsala University and Aalborg University, UPPAAL. Available from: <http://www.uppaal.com/>; Uppsala University and Aalborg University, UPPAAL. Available from: <http://www.uppaal.com/>
[33] Yovine, Sergio, KRONOS: a verification tool for real-time systems, Int. J. Softw. Tools Technol. Transfer, 1, 1-2, 123-133 (1997) · Zbl 1060.68606
[34] Zimmermann, Karel, A general separation theorem in extremal algebras, Ehkon. Mat. Obz., 13, 179-201 (1977) · Zbl 0365.90127
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.