Guardado en:
| Autores principales: | , , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2411.03160 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909532211380224 |
|---|---|
| author | Ghassemi, Fatemeh Zhiany, Saeed Abbasimoghadam, Nesa Hodaei, Ali Ataollahi, Ali Kovács, József Ábrahám, Erika Sirjani, Marjan |
| author_facet | Ghassemi, Fatemeh Zhiany, Saeed Abbasimoghadam, Nesa Hodaei, Ali Ataollahi, Ali Kovács, József Ábrahám, Erika Sirjani, Marjan |
| contents | Hybrid Rebeca is a modeling framework for asynchronous event-based cyber-physical systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. Besides the syntactical extension, we formalize the semantics of the extended language in terms of Timed Transition Systems, and adapt a reachability analysis algorithm originally designed for hybrid automata to be applicable to Hybrid Rebeca models. We prove the soundness of our approach and illustrate its applicability on a case study. The case study demonstrates that our dedicated algorithm is clearly superior to the alternative approach of transforming Hybrid Rebeca models to hybrid automata as an intermediate model and then applying the original reachability analysis method to this intermediate transformed models. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_03160 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Hybrid Rebeca Revisited Ghassemi, Fatemeh Zhiany, Saeed Abbasimoghadam, Nesa Hodaei, Ali Ataollahi, Ali Kovács, József Ábrahám, Erika Sirjani, Marjan Formal Languages and Automata Theory Hybrid Rebeca is a modeling framework for asynchronous event-based cyber-physical systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. Besides the syntactical extension, we formalize the semantics of the extended language in terms of Timed Transition Systems, and adapt a reachability analysis algorithm originally designed for hybrid automata to be applicable to Hybrid Rebeca models. We prove the soundness of our approach and illustrate its applicability on a case study. The case study demonstrates that our dedicated algorithm is clearly superior to the alternative approach of transforming Hybrid Rebeca models to hybrid automata as an intermediate model and then applying the original reachability analysis method to this intermediate transformed models. |
| title | Hybrid Rebeca Revisited |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2411.03160 |