Bhave et al. (2015):
PTA-BMC.
http://www.cse.iitb.ac.in/~devendra/pta-bmc.html.
Larsen et al. (2006):
UPPAAL-CORA.
http://people.cs.aau.dk/~adavid/cora/index.html.
Rajeev Alur & David L. Dill (1994):
A Theory of Timed Automata.
Theor. Comput. Sci 126(2),
pp. 183–235,
doi:10.1016/0304-3975(94)90010-8.
Rajeev Alur, Salvatore La Torre & George J. Pappas (2004):
Optimal Paths in Weighted Timed Automata.
Theor. Comput. Sci. 318,
pp. 297–322,
doi:10.1016/j.tcs.2003.10.038.
G. Audemard, A. Cimatti, A. Kornilowicz & R. Sebastiani (2002):
Bounded Model Checking for Timed Systems.
In: Formal Techniques for Networked and Distributed Sytems — FORTE 2002,
LNCS 2529.
Springer,
pp. 243–259,
doi:10.1007/3-540-36135-9_16.
Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Larsen, Paul Pettersson, Judi Romijn & Frits Vaandrager (2001):
Minimum-Cost Reachability for Priced Time Automata.
In: HSCC,
LNCS 2034.
Springer,
pp. 147–161,
doi:10.1007/3-540-45351-2_15.
Gerd Behrmann, Kim G Larsen & Jacob I Rasmussen (2005):
Optimal scheduling using priced timed automata.
Performance Evaluation Review 32(4),
pp. 34–40,
doi:10.1145/1059816.1059823.
Patricia Bouyer, Thomas Brihaye, Véronique Bruyère & Jean-François Raskin (2007):
On the Optimal Reachability Problem of Weighted Timed Automata.
FMSD 31(2),
pp. 135–175,
doi:10.1007/s10703-007-0035-4.
Patricia Bouyer, Ed Brinksma & Kim Guldstrand Larsen (2004):
Staying Alive as Cheaply as Possible.
In: HSCC,
pp. 203–218,
doi:10.1007/978-3-540-24743-2_14.
Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen & Nicolas Markey (2010):
Timed Automata with Observers Under Energy Constraints.
In: HSCC.
ACM,
pp. 61–70,
doi:10.1145/1755952.1755963.
Leonardo De Moura & Nikolaj Bjørner (2008):
Z3: An efficient SMT solver.
In: Tools and Algorithms for the Construction and Analysis of Systems.
Springer,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
Uli Fahrenberg & Kim G. Larsen (2009):
Discount-Optimal Infinite Runs in Priced Timed Automata.
ENTCS (INFINITY) 239,
pp. 179 – 191,
doi:10.1016/j.entcs.2009.05.039.
John Fearnley & Marcin Jurdzinski (2013):
Reachability in Two-Clock Timed Automata Is PSPACE-Complete.
In: ICALP,
pp. 212–223,
doi:10.1007/978-3-642-39212-2_21.
Dinko Ivanov, Marin Orli\'c, Cristina Seceleanu & Aneta Vulgarakis (2010):
REMES tool-chain: a set of integrated tools for behavioral modeling and analysis of embedded systems.
In: Automated software engineering.
ACM,
pp. 361–362,
doi:10.1145/1858996.1859076.
Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur & Rahul Mangharam (2012):
Modeling and verification of a dual chamber implantable pacemaker.
In: Tools and Algorithms for the Construction and Analysis of Systems.
Springer,
pp. 188–203,
doi:10.1007/978-3-642-28756-5_14.
M. Jongerden, A. Mereacre, H. Bohnenkamp, B. Haverkort & J. Katoen (2010):
Computing Optimal Schedules of Battery Usage in Embedded Systems.
Industrial Informatics, IEEE Transactions on 6(3),
pp. 276–286,
doi:10.1109/TII.2010.2051813.
Dejan Jovanovi\'c & Leonardo De Moura (2012):
Solving non-linear arithmetic.
In: Automated Reasoning.
Springer,
pp. 339–354,
doi:10.1007/978-3-642-31365-3_27.
Marcin Jurdzinski & Ashutosh Trivedi (2008):
Concavely-Priced Timed Automata.
In: FORMATS,
pp. 48–62,
doi:10.1007/978-3-540-85778-5_5.
F. Laroussinie, N. Markey & Ph. Schnoebelen (2004):
Model Checking Timed Automata with One or Two Clocks.
In: CONCUR,
LNCS 3170.
Springer,
pp. 387–401,
doi:10.1007/978-3-540-28644-8_25.
Marvin L. Minsky (1967):
Computation: finite and infinite machines.
Prentice-Hall, Inc..
eptcs@eptcs.org