Abstract
We provide a unifying view of timed models such as timed automata, probabilistic timed automata, and Markov automata. The timed models and their bisimulation semantics are encoded in the framework of uniform labeled transition systems. In this unifying framework, we show that the timed bisimilarities present in the literature can be re-obtained and that a new bisimilarity, of which we exhibit the modal logic characterization, can be introduced for timed models including probabilities. We finally highlight similarities and differences among the models.
Work partially supported by the MIUR-PRIN Project CINA and the European Commission FP7-ICT-FET Proactive Project TOPDRIM (grant agreement no. 318121).
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., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Bérard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae 36, 145–182 (1998)
Bernardo, M.: On the expressiveness of Markovian process calculi with durational and durationless actions. In: Proc. of GANDALF 2010. EPTCS, vol. 25, pp. 199–213 (2010)
Bernardo, M., De Nicola, R., Loreti, M.: A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences. Information and Computation 225, 29–82 (2013)
Cerans, K.: Decidability of bisimulation equivalences for parallel timer processes. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 302–315. Springer, Heidelberg (1993)
Corradini, F.: Absolute versus relative time in process algebras. Information and Computation 156, 122–172 (2000)
Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proc. of LICS 2010, pp. 342–351. IEEE-CS Press (2010)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32, 137–162 (1985)
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation 111, 193–244 (1994)
Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
Keller, R.M.: Formal verification of parallel programs. Communications of the ACM 19, 371–384 (1976)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282, 101–150 (2002)
Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Weak bisimulation for probabilistic timed automata. Theoretical Computer Science 411, 4291–4322 (2010)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94, 1–28 (1991)
Larsen, K.G., Yi, W.: Time abstracted bisimulation: Implicit specifications and decidability. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 160–176. Springer, Heidelberg (1994)
Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401–415. Springer, Heidelberg (1990)
Moller, F., Tofts, C.: Behavioural abstraction in TCCS. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 559–570. Springer, Heidelberg (1992)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD Thesis (1995)
Sproston, J., Troina, A.: Simulation and bisimulation for probabilistic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 213–227. Springer, Heidelberg (2010)
Yi, W.: CCS + Time = An Interleaving Model for Real Time Systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 217–228. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bernardo, M., Tesei, L. (2013). Encoding Timed Models as Uniform Labeled Transition Systems. In: Balsamo, M.S., Knottenbelt, W.J., Marin, A. (eds) Computer Performance Engineering. EPEW 2013. Lecture Notes in Computer Science, vol 8168. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40725-3_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-40725-3_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40724-6
Online ISBN: 978-3-642-40725-3
eBook Packages: Computer ScienceComputer Science (R0)