arxiv: Computer Science::Formal Languages and Automata Theory
LIDL(m) is a decidable fragment of Interval Duration Logic with Located Constraints, an expressive subset of dense-time Duration Calculus. It has been claimed that, for any LIDL(m) formula D, a timed automaton can be constructed which accepts the models of D. However, t... View more
 R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994.
 R. Alur, L. Fix, and T. Henzinger. Event-clock automata: a determinizable class of timed automata. Theoretical Computer Science, 211:253-273, 1999.
 R. Alur, L. Fix, and T. A. Henzinger. A determinizable class of timed automata. In Computer Aided Verification, CAV'94, LNCS 818, pages 1-13. Springer, 1994.
 R. Alur and T. Henzinger. Logics and models of real time: A survey. In Real-Time: Theory in Practice, REX Workshop, pages 74-106. Springer, 1991.
 E. Asarin, P. Caspi, and O. Maler. Timed regular expressions. J. ACM, 49(2):172-206, 2002.
 V. Braberman and D.V. Hung. On checking timed automata for linear duration invariants. In Proc. of the 19th IEEE Real-time Systems Symposium, pages 264-273, Piscataway, NJ, 1998. IEEE Press.
 J.R. Bu¨chi. On a decision method in restricted second-order arithmetic. Zeitschrift fu¨r Mathemathische Logik and Grundlagen der Mathematik, 6:66-92, 1960.
 C.C. Elgot. Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98:21-51, 1961.
 D. Guelev and D. Van Hung. On the completeness and decidability of Duration Calculus with iteration. Theoretical Computer Science, 337(1-3):278-304, 2005.
 J. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS '95, volume 1019 of LNCS, pages 89-110. Springer-Verlag, 1995.