References

1. Rajeev Alur & David L. Dill (1994): A Theory of Timed Automata. Theor. Comput. Sci. 126(2), pp. 183–235. Available at http://dx.doi.org/10.1016/0304-3975(94)90010-8.
2. Rajeev Alur & Thomas A. Henzinger (1993): Real-Time Logics: Complexity and Expressiveness. Inf. Comput. 104(1), pp. 35–77. Available at http://dx.doi.org/10.1006/inco.1993.1025.
3. Rajeev Alur & Thomas A. Henzinger (1994): A Really Temporal Logic. J. ACM 41(1), pp. 181–204. Available at http://doi.acm.org/10.1145/174644.174651.
4. Mikolaj Bojanczyk, Claire David, Anca Muscholl, Thomas Schwentick & Luc Segoufin (2011): Two-variable logic on data words. ACM Trans. Comput. Log. 12(4), pp. 27. Available at http://doi.acm.org/10.1145/1970398.1970403.
5. Benedikt Bollig (2011): An Automaton over Data Words That Captures EMSO Logic. In: Katoen & König, pp. 171–186. Available at http://dx.doi.org/10.1007/978-3-642-23217-6_12.
6. Benedikt Bollig, Aiswarya Cyriac, Paul Gastin & K. Narayan Kumar (2012): Model Checking Languages of Data Words. In: Lars Birkedal: FoSSaCS, LNCS 7213. Springer, pp. 391–405. Available at http://dx.doi.org/10.1007/978-3-642-28729-9_26.
7. Patricia Bouyer (2002): A logical characterization of data languages. Inf. Process. Lett. 84(2), pp. 75–85. Available at http://dx.doi.org/10.1016/S0020-0190(02)00229-6.
8. Patricia Bouyer, Fabrice Chevalier & Nicolas Markey (2010): On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), pp. 97–116. Available at http://dx.doi.org/10.1016/j.ic.2009.10.004.
9. Claudia Carapelle, Shiguang Feng, Oliver Fernandez Gil & Karin Quaas (2014): Satisfiability for MTL and TPTL over Non-monotonic Data Words. In: LATA, pp. 248–259. Available at http://dx.doi.org/10.1007/978-3-319-04921-2_20.
10. Stéphane Demri & Ranko Lazic (2009): LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3). Available at http://doi.acm.org/10.1145/1507244.1507246.
11. Stéphane Demri, Ranko Lazic & David Nowak (2007): On the freeze quantifier in Constraint LTL: Decidability and complexity. Inf. Comput. 205(1), pp. 2–24. Available at http://dx.doi.org/10.1016/j.ic.2006.08.003.
12. Stéphane Demri, Ranko Lazic & Arnaud Sangnier (2008): Model Checking Freeze LTL over One-Counter Automata. In: Roberto M. Amadio: FoSSaCS, LNCS 4962. Springer, pp. 490–504. Available at http://dx.doi.org/10.1007/978-3-540-78499-9_34.
13. Stéphane Demri & Arnaud Sangnier (2010): When Model-Checking Freeze LTL over Counter Machines Becomes Decidable. In: C.-H. Luke Ong: FOSSACS, LNCS 6014. Springer, pp. 176–190. Available at http://dx.doi.org/10.1007/978-3-642-12032-9_13.
14. Kousha Etessami & Thomas Wilke (1996): An Until Hierarchy for Temporal Logic. In: LICS. IEEE Computer Society, pp. 108–117. Available at http://doi.ieeecomputersociety.org/10.1109/LICS.1996.561310.
15. Joost-Pieter Katoen & Barbara König (2011): CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings. LNCS 6901. Springer. Available at http://dx.doi.org/10.1007/978-3-642-23217-6.
16. Ron Koymans (1990): Specifying Real-Time Properties with Metric Temporal Logic. Real-Time Systems 2(4), pp. 255–299. Available at http://dx.doi.org/10.1007/BF01995674.
17. Paritosh K. Pandya & Simoni S. Shah (2011): On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality, and Deterministic Freezing. In: Katoen & König, pp. 60–75. Available at http://dx.doi.org/10.1007/978-3-642-23217-6_5.
18. Luc Segoufin (2006): Automata and Logics for Words and Trees over an Infinite Alphabet. In: Zoltán Ésik: CSL, LNCS 4207. Springer, pp. 41–57. Available at http://dx.doi.org/10.1007/11874683_3.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org