Document Open Access Logo

Parametric Verification of Weighted Systems

Authors Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian Trier Ringsmose, Kim Guldstrand Larsen, Radu Mardare

PDF
Thumbnail PDF

File

OASIcs.SynCoP.2015.77.pdf
  • Filesize: 0.61 MB
  • 14 pages

Document Identifiers

Author Details

Peter Christoffersen
Mikkel Hansen
Anders Mariegaard
Julian Trier Ringsmose
Kim Guldstrand Larsen
Radu Mardare

Cite As Get BibTex

Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian Trier Ringsmose, Kim Guldstrand Larsen, and Radu Mardare. Parametric Verification of Weighted Systems. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 77-90, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/OASIcs.SynCoP.2015.77

Abstract

This paper addresses the problem of parametric model checking for weighted transition systems. We consider transition systems labelled with linear equations over a set of parameters and we use them to provide semantics for a parametric version of weighted CTL where the until and next operators are themselves indexed with linear equations. The parameters change the model-checking problem into a problem of computing a linear system of inequalities that characterizes the parameters that guarantee the satisfiability. To address this problem, we use parametric dependency graphs (PDGs) and we propose a global update function that yields an assignment
to each node in a PDG. For an iterative application of the function, we prove that a fixed point assignment to PDG nodes exists and the set of assignments constitutes a well-quasi ordering, thus ensuring that the fixed point assignment can be found after finitely many iterations. To demonstrate the utility of our technique, we have implemented a prototype tool that computes the constraints on parameters for model checking problems.

Subject Classification

Keywords
  • parametric weighted transition systems
  • parametric weighted CTL
  • parametric model checking
  • well-quasi ordering
  • tool

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In Logic in Computer Science, 1996. LICS'96. Proceedings., Eleventh Annual IEEE Symposium on, pages 313-321. IEEE, 1996. Google Scholar
  2. Rajeev Alur, Costas Courcoubetis, and David L. Dill. Model-checking in dense real-time. Inf. Comput., 104(1):2-34, 1993. Google Scholar
  3. Rajeev Alur and David L. Dill. Automata for modeling real-time systems. In ICALP, pages 322-335, 1990. Google Scholar
  4. Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA, pages 592-601, 1993. Google Scholar
  5. Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal paths in weighted timed automata. In HSCC, pages 49-62, 2001. Google Scholar
  6. Étienne André, Thomas Chatain, Laurent Fribourg, and Emmanuelle Encrenaz. An inverse method for parametric timed automata. International Journal of Foundations of Computer Science, 20(05):819-836, 2009. Google Scholar
  7. Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, and Frits W. Vaandrager. Minimum-cost reachability for priced timed automata. In HSCC, pages 147-161, 2001. Google Scholar
  8. Sine Viesmose Birch, Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, and Julian T. Ringsmose. Weighted transition system: From boolean to parametric analysis. 8th semester project at Aalborg University, Department of Computer Science, 2014. Google Scholar
  9. Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jirí Srba. Infinite runs in weighted timed automata with energy constraints. In FORMATS 2008. Proceedings, pages 33-47, 2008. Google Scholar
  10. Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, and Julian T. Ringsmose. Parametric verification of weighted systems. Unpublished Technical Report. http://pvtool.dk/tech_draft.pdf.
  11. Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, and Julian T. Ringsmose. Prototype tool. URL: http://pvtool.dk/.
  12. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample guided abstraction refinement. In Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, pages 154-169, 2000. Google Scholar
  13. Leonard Eugene Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics, 35(4):pp. 413-422, 1913. Google Scholar
  14. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1):63-92, 2001. Google Scholar
  15. Goran Frehse, Sumit Kumar Jha, and Bruce H. Krogh. A counterexample-guided approach to parameter synthesis for linear hybrid automata. In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, volume 4981 of Lecture Notes in Computer Science, pages 187-200. Springer Berlin Heidelberg, 2008. Google Scholar
  16. Thomas A. Henzinger and Howard Wong-Toi. Using hytech to synthesize control parameters for a steam boiler. In Jean-Raymond Abrial, Egon Börger, and Hans Langmaack, editors, Formal Methods for Industrial Applications, volume 1165 of Lecture Notes in Computer Science, pages 265-282. Springer Berlin Heidelberg, 1996. Google Scholar
  17. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(1):326-336, 1952. Google Scholar
  18. Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. Linear parametric model checking of timed automata. J. Log. Algebr. Program., 52-53:183-220, 2002. Google Scholar
  19. Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiří Srba, and Lars Kaerlund Oestergaard. Local model checking of weighted CTL with upper-bound constraints. In Model Checking Software, pages 178-195. Springer, 2013. Google Scholar
  20. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, 1990. Google Scholar
  21. Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134-152, 1997. Google Scholar
  22. Xinxin Liu and Scott A. Smolka. Simple linear-time algorithms for minimal fixed points. In Automata, Languages and Programming, pages 53-66. Springer, 1998. Google Scholar
  23. Chaiwat Sathawornwichit and Takuya Katayama. A parametric model checking approach for real-time systems design. In Software Engineering Conference, 2005. APSEC'05. 12th Asia-Pacific, pages 8-pp. IEEE, 2005. Google Scholar
  24. Alfred Tarski et al. A lattice-theoretical fixpoint theorem and its applications. Pacific journal of Mathematics, 5(2):285-309, 1955. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact