Abstract
We consider a general class of timed automata parameterized by a set of “input-determined” operators, in a continuous time setting. We show that for any such set of operators, we have a monadic second order logic characterization of the class of timed languages accepted by the corresponding class of automata. Further, we consider natural timed temporal logics based on these operators, and show that they are expressively equivalent to the first-order fragment of the corresponding MSO logics. As a corollary of these general results we obtain an expressive completeness result for the continuous version of MTL.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.A.: The Benefits of Relaxing Punctuality. Journal of the ACM 43(1), 116–146 (1996)
Raskin, J.F., Schobbens, P.Y.: State Clock Logic: A Decidable Real-Time Logic. In: HART, pp. 33–47 (1997)
D’Souza, D., Thiagarajan, P.S.: Product Interval Automata: A Subclass of Timed Automata. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 60–71. Springer, Heidelberg (1999)
D’Souza, D., Raj Mohan, M.: Eventual Timed Automata. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 322–334. Springer, Heidelberg (2005)
D’Souza, D., Tabareau, N.: On timed automata with input-determined guards. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 68–83. Springer, Heidelberg (2004)
Koymans, R.: Specifying Real-Time Properties with Metric Temporal Logic. Real-Time Systems 2(4), 255–299 (1990)
Ouaknine, J., Worrel, J.: On the Decidability of Metric Temporal Logic. In: LICS, pp. 188–197. IEEE Computer Society, Los Alamitos (2005)
Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 432–443. Springer, Heidelberg (2005)
Prabhakar, P., D’Souza, D.: On the expressiveness of MTL with past operators. Technical Report IISc-CSA-TR-2006-5 Indian Institute of Science, Bangalore 560012, India (May 2006), URL: http://archive.csa.iisc.ernet.in/TR/2006/5/
Henzinger, T.A., Raskin, J.F., Schobbens, P.Y.: The Regular Real-Time Languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 580–591. Springer, Heidelberg (1998)
Rabinovich, A.M.: Finite variability interpretation of monadic logic of order. Theor. Comput. Sci. 275(1-2), 111–125 (2002)
Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, California (1968)
Raskin, J.F.: Logics, Automata and Classical Theories for Deciding Real-Time. PhD thesis, FUNDP, Belgium (1999)
Chevalier, F., D’Souza, D., Prabhakar, P.: On continuous timed automata with input-determined guards. Technical Report IISc-CSA-TR-2006-7 Indian Institute of Science, Bangalore 560012, India (June 2006), URL: http://archive.csa.iisc.ernet.in/TR/2006/7/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chevalier, F., D’Souza, D., Prabhakar, P. (2006). On Continuous Timed Automata with Input-Determined Guards. In: Arun-Kumar, S., Garg, N. (eds) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2006. Lecture Notes in Computer Science, vol 4337. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11944836_34
Download citation
DOI: https://doi.org/10.1007/11944836_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-49994-7
Online ISBN: 978-3-540-49995-4
eBook Packages: Computer ScienceComputer Science (R0)