Abstract
We address the problem of synthesizing a timed automaton from a set of optimised timed scenarios, and present a simple, efficient algorithm that solves the problem. Under a simplifying assumption about the set of scenarios we show that our synthesized automaton has the minimal number of clocks in the entire class of language-equivalent automata.
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
Similar content being viewed by others
Notes
- 1.
For a timed automaton with |K| clocks, the number of clock regions is at most \(R=|K|! 4^{|K|} \varPi _{x\in K} (\mu _x+1)\), where \(\mu _x\) is the maximum constant with which clock x is compared [12].
- 2.
- 3.
The notion of “behaviour” is equivalent to that of Alur’s “timed word” [15]. We found the term “behaviour” more suitable and intuitive in the context of timed scenarios.
- 4.
To keep the presentation compact, sharp inequalities are not allowed [11]. Equality is expressed in terms of \(\le \) and \(\ge \).
- 5.
Equality will be expressed directly using \(=\) in the external representation.
- 6.
The absence of an upper bound for some i and j will be denoted by \(M_{i j}^{\xi } = \infty \).
- 7.
- 8.
That is, a constraint cannot be removed without changing the semantics.
- 9.
Optimality was achieved under the assumption that a timed scenario cannot be split into two [13].
- 10.
If \(\alpha \) is of the form \(\tau _{i_1,j_1} \ge a\), and/or \(\beta \) is of the form \(\tau _{i_2,j_2} \ge b\), the steps of the proof will be essentially the same.
- 11.
It is impossible for both \(\tau _{i_1,j} \le u\) and \(M_{i_1 j_1}^{\eta } = c\) to be implied, without anchor \(i_1\).
- 12.
If the explicit constraints of two scenarios differ only on constraints between one pair of events, their combination cannot include zigzagging behaviours [14].
- 13.
An implementation in C++ can be made available upon request.
References
Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.): FORTE 2008. LNCS, vol. 5048. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68855-6
Greenyer, J.: Scenario-based modeling and programming of distributed systems, In: M. Köhler-Bussmeier, E. Kindler, H. Rölke (Eds.), In: Proceedings of the International Workshop on Petri Nets and Software Engineering 2021 co-located with the 42nd International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2021), Paris, France, June 25th, 2021 (due to COVID-19: virtual conference), Vol. 2907 of CEUR Workshop Proceedings, CEUR-WS.org, pp. 241–252 (2021)
Somé, S., Dssouli, R., Vaucher, J.: From scenarios to timed automata: building specifications from users requirements. In: Proceedings of the Second Asia Pacific Software Engineering Conference, APSEC 1995, IEEE Computer Society, pp. 48–57
Chandrasekaran, P., Mukund, M.: Matching scenarios with timing constraints. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 98–112. Springer, Heidelberg (2006). https://doi.org/10.1007/11867340_8
Harel, D., Kugler, H., Pnueli, A.: Synthesis revisited: generating statechart models from scenario-based requirements. In: Kreowski, H.-J., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol. 3393, pp. 309–324. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31847-7_18
Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans. Softw. Eng. 29(2), 99–115 (2003)
Akshay, S., Mukund, M., Kumar, K.N.: Checking coverage for infinite collections of timed scenarios. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 181–196. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_13
Bollig, B., Katoen, J.-P., Kern, C., Leucker, M.: Replaying play in and play out: synthesis of design models from scenarios by learning. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 435–450. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_33
Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 75–91. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-13338-6_7
Saeedloei, N., Kluźniak, F.: From scenarios to timed automata. In: Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Proceedings, pp. 33–51
Saeedloei, N., Kluźniak, F.: Timed scenarios: consistency, equivalence and optimization. In: Massoni, T., Mousavi, M.R. (eds.) SBMF 2018. LNCS, vol. 11254, pp. 215–233. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03044-5_14
Alur, R., Madhusudan, P.: Decision problems for timed automata: a survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_1
Campos, S., Minea, M. (eds.): SBMF 2021. LNCS, vol. 13130. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-92137-8
Saeedloei, N., Kluźniak, F.: Operations on timed scenarios. In: M. Huisman, A. Ravara (Eds.), Formal Techniques for Distributed Objects, Components, and Systems - 43rd IFIP WG 6.1 International Conference, FORTE 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings, Vol. 13910 of Lecture Notes in Computer Science, Springer, pp. 97–114 (2023) https://doi.org/10.1007/978-3-031-35355-0_7
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1089–1101. Springer, Heidelberg (2005). https://doi.org/10.1007/11523468_88
Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When are timed automata determinizable? In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 43–54. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02930-1_4
Saeedloei, N., Kluźniak, F.: Optimization of timed scenarios. In: G. Carvalho, V. Stolz (Eds.), Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings, Vol. 12475 of Lecture Notes in Computer Science, Springer, pp. 119–136 (2020) https://doi.org/10.1007/978-3-031-22476-8
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_17
Saeedloei, N., Kluźniak, F.: Observations about timed scenarios. https://tigerweb.towson.edu/nsaeedloei/Observations.pdf
Saeedloei, N., Kluźniak, F.: Clock allocation in timed automata and graph colouring. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC 2018, pp. 71–80. https://doi.org/10.1145/3178126.3178138
N. Saeedloei, F. Kluźniak, Synthesizing clock-efficient timed automata, in: B. Dongol, E. Troubitsyna (Eds.), Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings, Vol. 12546 of Lecture Notes in Computer Science, Springer, 2020, pp. 276–294. https://doi.org/10.1007/978-3-031-07727-2
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 IFIP International Federation for Information Processing
About this paper
Cite this paper
Saeedloei, N., Kluźniak, F. (2024). Synthesizing Timed Automata with Minimal Numbers of Clocks from Optimised Timed Scenarios. In: Castiglioni, V., Francalanza, A. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2024. Lecture Notes in Computer Science, vol 14678. Springer, Cham. https://doi.org/10.1007/978-3-031-62645-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-031-62645-6_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-62644-9
Online ISBN: 978-3-031-62645-6
eBook Packages: Computer ScienceComputer Science (R0)