Abstract
In this paper, we study the complexity of model-checking formulas of three important real-time logics (MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are (i) a single finite (or ultimately periodic) timed path, (ii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.
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.
Similar content being viewed by others
References
Alur, R., Courcoubetis, C., Dill, D.L.: Model-Checking in Dense Real-Time. Information and Computation 104(1), 2–34 (1993)
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)
Alur, R., Henzinger, T.A.: A Really Temporal Logic. Journal of the ACM 41(1), 181–203 (1994)
Alur, R., Kurshan, R.P., Viswanathan, M.: Membership Question for Timed and Hybrid Automata. In: Proc. 19th Symp. Real-Time Systems (RTS 98), December 1998, pp. 254–263. IEEE Comp. Soc. Press, Los Alamitos (1998)
Bouajjani, A., Tripakis, S., Yovine, S.: On-the-Fly Symbolic Model Checking for Real-Time Systems. In: Proc. 18th Symp. Real-Time Systems (RTS 1997), December 1997, pp. 25–35. IEEE Comp. Soc. Press, Los Alamitos (1997)
Bruyère, V., Dall’Olio, E., Raskin, J.-F.: Durations, Parametric Model Checking in Timed Automata with Presburger Arithmetic. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 687–698. Springer, Heidelberg (2003)
Courcoubetis, C., Yannakakis, M.: Minimum and Maximum Delay Problems in Real-Time Systems. Formal Methods in System Design 1(4), 385–415 (1992)
Manna, Z., Pnueli, A.: Verifying Hybrid Systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 4–35. Springer, Heidelberg (1993)
Markey, N., Schnoebelen, P.: Model Checking a Path. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 251–265. Springer, Heidelberg (2003)
Thati, P., Roşu, G.: Monitoring Algorithms for Metric Temporal Logic Specifications. In: Havelund, K., Roşu, G. (eds.) Proc. 4th Intl Workshop on Runtime Verification (RV 2004), April 2004. ENTCS, pp. 131–147. Elsevier Science, Amsterdam (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Markey, N., Raskin, JF. (2004). Model Checking Restricted Sets of Timed Paths. In: Gardner, P., Yoshida, N. (eds) CONCUR 2004 - Concurrency Theory. CONCUR 2004. Lecture Notes in Computer Science, vol 3170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28644-8_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-28644-8_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22940-7
Online ISBN: 978-3-540-28644-8
eBook Packages: Springer Book Archive