Abstract
A decidability result and a model-checking procedure for a rich subset of Duration Calculus (DC) [19] is obtained through reductions to first-order logic over the real-closed field and to Multi-Priced Timed Automata (MPTA) [13]. In contrast to other reductions of fragments of DC to reachability problems in timed automata, the reductions do also cover constraints on positive linear combinations of accumulated durations. By being able to handle accumulated durations under chop as well as in arbitrary positive Boolean contexts, the procedures extend the results of Zhou et al. [22] on decidability of linear duration invariants to a much wider fragment of DC.
This work has been supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, www.avacs.org) and by Velux Fonden, Søborg, Denmark, through the Velux Visiting Professors Programme.
Chapter PDF
Similar content being viewed by others
Keywords
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Comput. Sci. 126(2), 183–235 (1994)
Asarin, E., Caspi, P., Maler, O.: A Kleene theorem for timed automata. In: Winskel, G. (ed.) 12th Annual IEEE Symposium on Logic in Computer Science (LICS’97), IEEE Computer Society Press, Los Alamitos (1997)
Audemard, G., et al.: A SAT-based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 193–208. Springer, Heidelberg (2002)
Bengtsson, J., et al.: Uppaal – a tool suite for automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)
Bouajjani, A., Lakhnech, Y., Robbana, R.: From duration calculus to linear hybrid automata. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, Springer, Heidelberg (1995)
Dierks, H.: Synthesizing controllers from real-time specifications. In: Tenth International Symposium on System Synthesis (ISSS ‘97), pp. 126–133. IEEE Computer Society Press, Los Alamitos (1997)
Fränzle, M.: Controller Design from Temporal Logic: Undecidability need not matter. Dissertation, Technische Fakultät der Chr.-Albrechts-Universität Kiel, Germany (1997)
Fränzle, M.: Model-checking dense-time duration calculus. Formal Aspects of Computing 16(2), 121–139 (2004)
Fränzle, M., Herde, C.: Efficient proof engines for bounded model checking of hybrid systems. In: Bicarregui, J., Butterfield, A., Arenas, A. (eds.) Proceedings Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 04). Electronic Notes in Theoretical Computer Science, vol. 133, pp. 119–137. Elsevier Science B.V, Amsterdam (2005)
Halpern, J., Moszkowski, B., Manna, Z.: A hardware semantics based on temporal intervals. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 278–291. Springer, Heidelberg (1983)
Hoenicke, J.: Combination of Processes, Data and Time. Dissertation, Carl von Ossietzky Universität, Oldenburg, Germany (2006)
Laknech, Y.: Specification and Verification of Hybrid and Real-Time Systems. Dissertation, Technische Fakultät der Chr.-Albrechts-Universität Kiel, Germany (1996)
Larsen, K.G., Rasmussen, J.I.: Optimal conditional reachability for multi-priced timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 230–244. Springer, Heidelberg (2005)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, vol. 1. Springer, Heidelberg (1992)
Olderog, E.-R., Dierks, H.: Decomposing real-time specifications. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, Springer, Heidelberg (1998)
Ravn, A.P.: Design of Embedded Real-Time Computing Systems. Doctoral dissertation, Department of Computer Science, Danish Technical University, Lyngby, DK (Oct. 1995), Available as technical report ID-TR 1995-170.
Sharma, P., Pandya, P.K., Chakraborty, S.: Bounded validity checking of interval duration logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, Springer, Heidelberg (2005)
Tarski, A.: A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica (1948)
Zhou, C., Hansen, M.R.: Duration Calculus — A Formal Approach to Real-Time Systems. EATCS monographs on theoretical computer science. Springer, Heidelberg (2004)
Zhou, C., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol. 665, pp. 58–68. Springer, Heidelberg (1993)
Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Zhou, C., et al.: Linear duration invariants. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 86–109. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Fränzle, M., Hansen, M.R. (2007). Deciding an Interval Logic with Accumulated Durations. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)