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