Unknown Biases and Timing Constraints in Timed Automata
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909127358283776 |
|---|---|
| author | Haase, Darion Katoen, Joost-Pieter |
| author_facet | Haase, Darion Katoen, Joost-Pieter |
| contents | Timed automata are the formal model for real-time systems. Extensions with discrete probabilistic branching have been considered in the literature and successfully applied. Probabilistic timed automata (PTA) do require all branching probabilities and clock constraints to be constants. This report investigates PTA in which this constraint is relaxed: both branching probabilities and clock constraints can be parametric. We formally define this PTA variant and define its semantics by an uncountable parametric Markov Decision Process (pMDP). We show that reachability probabilities in parametric L/U-PTA can be reduced to considering PTA with only parametric branching probabilities. This enables the usage of existing techniques from the literature. Finally, we generalize the symbolic backward and digital clock semantics of PTA to the setting with parametric probabilities and constraints. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_02210 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Unknown Biases and Timing Constraints in Timed Automata Haase, Darion Katoen, Joost-Pieter Logic in Computer Science Formal Languages and Automata Theory Timed automata are the formal model for real-time systems. Extensions with discrete probabilistic branching have been considered in the literature and successfully applied. Probabilistic timed automata (PTA) do require all branching probabilities and clock constraints to be constants. This report investigates PTA in which this constraint is relaxed: both branching probabilities and clock constraints can be parametric. We formally define this PTA variant and define its semantics by an uncountable parametric Markov Decision Process (pMDP). We show that reachability probabilities in parametric L/U-PTA can be reduced to considering PTA with only parametric branching probabilities. This enables the usage of existing techniques from the literature. Finally, we generalize the symbolic backward and digital clock semantics of PTA to the setting with parametric probabilities and constraints. |
| title | Unknown Biases and Timing Constraints in Timed Automata |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2403.02210 |