Abstract
We introduce the novel notion of quasi-equal clocks and use it to improve the verification time of networks of timed automata. Intuitively, two clocks are quasi-equal if, during each run of the system, they have the same valuation except for those points in time where they are reset. We propose a transformation that takes a network of timed automata and yields a network of timed automata which has a smaller set of clocks and preserves properties up to those not comparing quasi-equal clocks. Our experiments demonstrate that the verification time in three transformed real world examples is much lower compared to the original.
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.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Rappaport, T.S.: Wireless communications: principles and practice, vol 2. Prentice Hall (2002)
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D., Olivero, A.: Speeding Up Model Checking of Timed-Models by Combining Scenario Specialization and Live Component Analysis. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 58–72. Springer, Heidelberg (2009)
Braberman, V.A., Garbervetsky, D., Olivero, A.: Improving the Verification of Timed Systems Using Influence Information. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 21–36. Springer, Heidelberg (2002)
Bozga, M., Fernandez, J.-C., Ghirvu, L.: State Space Reduction Based on Live Variables Analysis. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 164–178. Springer, Heidelberg (1999)
Lugiez, D., Niebert, P., Zennou, S.: A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 296–311. Springer, Heidelberg (2004)
Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: RTSS, pp. 73–81. IEEE (1996)
Daws, C., Tripakis, S.: Model Checking of Real-Time Reachability Properties Using Abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)
Muñiz, M., Westphal, B., Podelski, A.: Timed Automata with Disjoint Activity. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 188–203. Springer, Heidelberg (2012)
Salah, R., Bozga, M., Maler, O.: Compositional timing analysis. In: EMSOFT, pp. 39–48. ACM (2009)
Olderog, E.-R., Dierks, H.: Real-time systems - formal specification and automatic verification. Cambridge University Press (2008)
Gobriel, S., Khattab, S., Mossé, D., Brustoloni, J., Melhem, R.: Ridesharing: Fault tolerant aggregation in sensor networks using corrective actions. the 3rd annual. In: IEEE Communications Society Conference on Sensor, Mesh and Ad Hoc Communications and Networks (SECON), pp. 595–604 (2006)
Jensen, H., Larsen, K., Skou, A.: Modelling and analysis of a collision avoidance protocol using SPIN and Uppaal. In: 2nd SPIN Workshop (1996)
Dietsch, D., Feo-Arenis, S., Westphal, B., Podelski, A.: Disambiguation of industrial standards through formalization and graphical languages. In: RE, pp. 265–270 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herrera, C., Westphal, B., Feo-Arenis, S., Muñiz, M., Podelski, A. (2012). Reducing Quasi-Equal Clocks in Networks of Timed Automata. In: Jurdziński, M., Ničković, D. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2012. Lecture Notes in Computer Science, vol 7595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33365-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-33365-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33364-4
Online ISBN: 978-3-642-33365-1
eBook Packages: Computer ScienceComputer Science (R0)