Top

Published in:

2025 | OriginalPaper | Chapter

On the Existence of Unions of Timed Scenarios

Author : Neda Saeedloei

Published in: Formal Methods: Foundations and Applications

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

In earlier work it was shown that, given two consistent timed scenarios, there might not exist a scenario whose semantics is the union of those of the two. A sufficient condition for the non-existence of such a union was also identified. In this paper we report on a comprehensive study of the union operation for scenarios. We identify a new sufficient condition that provides a syntactic criterion for the existence of a scenario that is the union of two given scenarios. We also prove that the condition is necessary.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

next chapter SMTQuery: Analysing SMT-LIB String Benchmarks

The notion of “behaviour” is equivalent to that of Alur’s “timed word” [15].

The aim of optimization which begins with the construction of a stable distance table, is to obtain a minimal set of constraints, i.e., removal of any of these constraints would change the semantics.

There are three other cases, which can be obtained from these by replacing i and j with k and l, and vice versa. The proofs can be obtained by interchanging i and k, as well as j and l.

If \(k=i\), then \(t_{ki } = 0\), hence \(t_{ki} \in I _{k i} = [0,0]\). Similarly, if \(j=l\), then \(t_{jl } = 0\), hence \(t_{jl} \in I _{j l} = [0,0]\).

See the diagrams in Figs. 6 and 7.

In the definition it is assummed that ij is within \(\xi \) and kl is within \(\eta \). There are three other cases where ij is within \(\eta \) and kl is within \(\xi \). Those cases are symmetric and can be obtained by interchanging \(\xi \) and \(\eta \).

Salah, A., Mizouni, R., Dssouli, R., Parreaux, B.: Formal composition of distributed scenarios. In: de Frutos-Escrig, D., Núñez, M. (eds.) Formal Techniques for Networked and Distributed Systems - FORTE 2004, pp. 213–228. Springer Berlin Heidelberg, Berlin, Heidelberg (2004)View Article
Greenyer, J.: Scenario-based modeling and programming of distributed systems. In: Köhler-Bussmeier, M., Kindler, E., Rölke, H. (eds.) 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 ’95, IEEE Computer Society, pp. 48–57
Chandrasekaran, P., Mukund, M.: Matching scenarios with timing constraints. In: Asarin, E., Bouyer, P. (eds.) Formal Modeling and Analysis of Timed Systems, pp. 98–112. Springer, Berlin, Heidelberg (2006)View Article
Harel, D., Kugler, H., Pnueli, A.: Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements, pp. 309–324. Springer, Berlin Heidelberg (2005)
Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans. Softw. Eng. 29(2), 99–115 (2003)View Article
Akshay, S., Mukund, M., Kumar, K.N.: Checking coverage for infinite collections of timed scenarios. In: CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Proceedings, pp. 181–196
Bollig, B., Katoen, J., Kern, C., Leucker, M.: Replaying play in and play out: synthesis of design models from scenarios by learning. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pp. 435–450 (2007)
Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing Finite-State Protocols from Scenarios and Requirements. In: Yahav, E. (ed.) Hardware and Software: Verification and Testing, pp. 75–91. Springer International Publishing, Cham (2014)View Article
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: Formal Methods: Foundations and Applications - 21st Brazilian Symposium, SBMF 2018, Proceedings, pp. 215–233
Saeedloei, N., Kluźniak, F.: Optimization of timed scenarios. In: Carvalho, G., Stolz, V. (eds.) Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25–27, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12475, pp. 119–136. Springer (2020)
Saeedloei, N., Kluźniak, F.: Operations on timed scenarios. In: Huisman, M., Ravara, A. (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. Lecture Notes in Computer Science, Vol. 13910, pp. 97–114. Springer (2023). https://doi.org/10.1007/978-3-031-35355-0_7
Saeedloei, N., Kluźniak, F.: Synthesizing timed automata with minimal numbers of clocks from optimized timed scenarios. In: Formal Techniques for Distributed Objects, Components, and Systems - International Conference, FORTE 2024, Proceedings, To appear
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)MathSciNetView Article
Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 1384, pp. 313–329. Springer-Verlag (1998). https://doi.org/10.1007/BFb0054180
Balarin, F.: Approximate reachability analysis of timed automata. In: 17th IEEE Real-Time Systems Symposium, pp. 52–61 (1996). https://doi.org/10.1109/REAL.1996.563700
Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: 18th IEEE Real-Time Systems Symposium, pp. 14–24 (1997)
Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data-structures for the verification of timed automata. In: Maler, O. (ed.) Hybrid and Real-Time Systems, pp. 346–360. Springer Berlin Heidelberg, Berlin, Heidelberg (1997)View Article
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, pp. 197–212. Springer-Verlag New York, Inc. (1990)
Bozga, M., Maler, O., Pnueli, A., Yovine, S.: Some progress in the symbolic verification of timed automata. In: Grumberg, O. (ed.) Computer Aided Verification, pp. 179–190. Springer Berlin Heidelberg, Berlin, Heidelberg (1997)View Article
Saeedloei, N., Kluźniak, F.: Minimization of the number of clocks for timed scenarios. In: Campos, S., Minea, M. (eds.) Formal Methods: Foundations and Applications - 24th Brazilian Symposium, SBMF 2021 Proceedings. Lecture Notes in Computer Science, vol. 13130, pp. 122–139. Springer (2021)
Saeedloei, N.: On the Existence of Unions of Timed Scenarios. https://tigerweb.towson.edu/nsaeedloei/thech-report-union.pdf
Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets: Advances in Petri Nets, pp. 87–124. Springer Berlin Heidelberg, Berlin, Heidelberg (2004)View Article
Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D. (eds.) Computer Aided Verification, pp. 341–353. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)View Article

Title: On the Existence of Unions of Timed Scenarios
Author: Neda Saeedloei
Publisher: Springer Nature Switzerland
Book: Formal Methods: Foundations and Applications
Print ISBN: 978-3-031-78115-5

Electronic ISBN: 978-3-031-78116-2

Copyright Year: 2025
DOI: https://doi.org/10.1007/978-3-031-78116-2_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"