Cargando…
Verified Certification of Reachability Checking for Timed Automata
Prior research has shown how to construct a mechanically verified model checker for timed automata, a popular formalism for modeling real-time systems. In this paper, we shift the focus from verified model checking to certifying unreachability. This allows us to benefit from better approximation ope...
Autores principales: | Wimmer, Simon, Mutius, Joshua von |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7439749/ http://dx.doi.org/10.1007/978-3-030-45190-5_24 |
Ejemplares similares
-
Timed Automata Relaxation for Reachability
por: Bendík, Jaroslav, et al.
Publicado: (2021) -
AVR: Abstractly Verifying Reachability
por: Goel, Aman, et al.
Publicado: (2020) -
Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
por: Funke, Florian, et al.
Publicado: (2020) -
Action-Based Model Checking: Logic, Automata, and Reduction
por: Siegel, Stephen F., et al.
Publicado: (2020) -
Bounded Model Checking for Metric Temporal Logic Properties of Timed Automata with Digital Clocks †
por: Zbrzezny, Agnieszka M., et al.
Publicado: (2022)