Regular hedge model checking
We extend the regular model checking framework so that it can handle systems with arbitrary width tree-like structures. Con gurations of a system are represented by trees of arbitrary arities, sets of con gurations are represented by regular hedge automata, and the dynamics of a system is modeled by...
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Objeto de conferencia |
| Lenguaje: | Inglés |
| Publicado: |
2006
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/24400 |
| Aporte de: |
| id |
I19-R120-10915-24400 |
|---|---|
| record_format |
dspace |
| institution |
Universidad Nacional de La Plata |
| institution_str |
I-19 |
| repository_str |
R-120 |
| collection |
SEDICI (UNLP) |
| language |
Inglés |
| topic |
Ciencias Informáticas Model checking Frameworks Mutual exclusion Trees |
| spellingShingle |
Ciencias Informáticas Model checking Frameworks Mutual exclusion Trees D'Orso, Julien Touili, Tayssir Regular hedge model checking |
| topic_facet |
Ciencias Informáticas Model checking Frameworks Mutual exclusion Trees |
| description |
We extend the regular model checking framework so that it can handle systems with arbitrary width tree-like structures. Con gurations of a system are represented by trees of arbitrary arities, sets of con gurations are represented by regular hedge automata, and the dynamics of a system is modeled by a regular hedge transducer. We consider the problem of computing the transitive closure T + of a regular hedge transducer T. This construction is not possible in general.
Therefore, we present a general acceleration technique for computing T+. Our method consists of enhancing the termination of the iterative computation of the different compositions Ti by merging the states of the hedge transducers according to an appropriate equivalence relation that preserves the traces of the transducers. We provide a methodology for effectively deriving equivalence relations that are appropriate. We have successfully applied our technique to compute transitive closures for some mutual exclusion protocols de ned on arbitrary width tree topologies, as well as for an XML application. |
| format |
Objeto de conferencia Objeto de conferencia |
| author |
D'Orso, Julien Touili, Tayssir |
| author_facet |
D'Orso, Julien Touili, Tayssir |
| author_sort |
D'Orso, Julien |
| title |
Regular hedge model checking |
| title_short |
Regular hedge model checking |
| title_full |
Regular hedge model checking |
| title_fullStr |
Regular hedge model checking |
| title_full_unstemmed |
Regular hedge model checking |
| title_sort |
regular hedge model checking |
| publishDate |
2006 |
| url |
http://sedici.unlp.edu.ar/handle/10915/24400 |
| work_keys_str_mv |
AT dorsojulien regularhedgemodelchecking AT touilitayssir regularhedgemodelchecking |
| bdutipo_str |
Repositorios |
| _version_ |
1764820466027986945 |