Luca de Alfaro, Marco Faella & Mariëlle Stoelinga (2009):
Linear and Branching System Metrics.
IEEE Trans. Software Eng. 35(2),
pp. 258–273,
doi:10.1109/TSE.2008.106.
Rajeev Alur & David L. Dill (1990):
Automata For Modeling Real-Time Systems.
In: Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, July 16-20, 1990, Proceedings,
pp. 322–335,
doi:10.1007/BFb0032042.
Rajeev Alur, Thomas A. Henzinger & Moshe Y. Vardi (1993):
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,
pp. 592–601,
doi:10.1145/167088.167242.
Étienne André, Thomas Chatain, Laurent Fribourg & Emmanuelle Encrenaz (2009):
An Inverse Method for Parametric Timed Automata.
International Journal of Foundations of Computer Science 20(5),
pp. 819–836,
doi:10.1142/S0129054109006905.
Étienne André, Yang Liu, Jun Sun & Jin Song Dong (2014):
Parameter synthesis for hierarchical concurrent real-time systems.
Real-Time Systems 50(5-6),
pp. 620–679,
doi:10.1007/s11241-014-9208-6.
Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn & Frits W. Vaandrager (2001):
Minimum-Cost Reachability for Priced Timed Automata.
In: Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings,
pp. 147–161,
doi:10.1007/3-540-45351-2_15.
Nikolaj Bjørner, Anh-Dung Phan & Lars Fleckenstein (2015):
νLaTeX Error: Bad math environment delimiterSee the LaTeX manual or LaTeX Companion for explanation.Your command was ignored.Type I <command> <return> to replace it with another command,or <return> to continue without it.Z - An Optimizing SMT Solver.
In: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings,
pp. 194–199,
doi:10.1007/978-3-662-46681-0_14.
Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey & JiríSrba (2008):
Infinite Runs in Weighted Timed Automata with Energy Constraints.
In: Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings,
pp. 33–47,
doi:10.1007/978-3-540-85778-5_4.
Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian Trier Ringsmose, Kim Guldstrand Larsen & Radu Mardare (2015):
Parametric Verification of Weighted Systems.
In: Étienne André & Goran Frehse: 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15),
OpenAccess Series in Informatics (OASIcs) 44.
Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik,
Dagstuhl, Germany,
pp. 77–90,
doi:10.4230/OASIcs.SynCoP.2015.77.
Available at http://drops.dagstuhl.de/opus/volltexte/2015/5611.
E. Allen Emerson & Richard J. Trefler (1999):
Parametric Quantitative Temporal Reasoning.
In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999,
pp. 336–343,
doi:10.1109/LICS.1999.782628.
Louise Foshammer, Kim Guldstrand Larsen & Bingtian Xue (2016):
Logical Characterization and Complexity of Weighted Branching Preorders and Distances.
In: Proceedings of The Seventh International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking, COMPUTATION TOOLS 2016, Rome, Italy, March 20-24, 2016..
IARIA XPS Press,
pp. To Appear.
Rob J. van Glabbeek & W. P. Weijland (1996):
Branching Time and Abstraction in Bisimulation Semantics.
J. ACM 43(3),
pp. 555–600,
doi:10.1145/233551.233556.
Ernst Moritz Hahn, Tingting Han & Lijun Zhang (2011):
Synthesis for PCTL in Parametric Markov Decision Processes.
In: NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings,
pp. 146–161,
doi:10.1007/978-3-642-20398-5_12.
Ernst Moritz Hahn, Holger Hermanns, Björn Wachter & Lijun Zhang (2010):
PARAM: A Model Checker for Parametric Markov Models.
In: Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings,
pp. 660–664,
doi:10.1007/978-3-642-14295-6_56.
Michal Knapik & Wojciech Penczek (2014):
Parameter Synthesis for Timed Kripke Structures.
Fundam. Inform. 133(2-3),
pp. 211–226,
doi:10.3233/FI-2014-1072.
Kim G. Larsen, Uli Fahrenberg & Claus R. Thrane (2011):
Metrics for weighted transition systems: Axiomatization and complexity.
Theor. Comput. Sci. 412(28),
pp. 3358–3369,
doi:10.1016/j.tcs.2011.04.003.
Robin Milner (1989):
Communication and concurrency.
PHI Series in computer science.
Prentice Hall.
Leonardo Mendonça de Moura & Nikolaj Bjørner (2008):
Z3: An Efficient SMT Solver.
In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
David Park (1981):
Theoretical Computer Science: 5th GI-Conference Karlsruhe, March 23–25, 1981, chapter Concurrency and automata on infinite sequences,
pp. 167–183.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
doi:10.1007/BFb0017309.
Alfred Tarski (1955):
A lattice-theoretical fixpoint theorem and its applications.
Pacific journal of Mathematics 5(2),
pp. 285–309,
doi:10.2140/pjm.1955.5.285.
Claus R. Thrane, Uli Fahrenberg & Kim G. Larsen (2010):
Quantitative analysis of weighted transition systems.
J. Log. Algebr. Program. 79(7),
pp. 689–703,
doi:10.1016/j.jlap.2010.07.010.
eptcs@eptcs.org