Distributed Event Clock Automata: Extended abstract

James Ortiz Vega; Axel Legay; Pierre-Yves Schobbens

doi:10.1007/978-3-642-22256-6_23

Distributed Event Clock Automata: Extended abstract

James Ortiz Vega, Axel Legay, Pierre-Yves Schobbens

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférence › Article dans les actes d'une conférence/un colloque

281 Téléchargements (Pure)

Résumé

Dans les systèmes temps réel distribués, les horloges ne sont pas parfaitement synchronisées. Pour modéliser ceci, nous définissons les horloges indépendantes et leur sémantique. L'inclusion de langages d'automates temporisés à horloges indépendantes (icTA) est indécidable. C'est pourquoi nous proposons les horloges d'événements récursifs sindépendantes et leurs automates (DECA). Ils admettent toutes les opérations booléennes, et leur inclusion de langages est décidable (plus précisément, complète en espace polynomial), ce qui permet un développement par raffinements successifs. Nous proposons aussi la logique DECTL, une logique temps réel basée sur des évolutions temporelles indépendantes. On peut vérifier les modèles de cette logique en traduisant les formules en automates DECA.

langue originale	Anglais
titre	CIAA 2011
Sous-titre	16th International Conference on Implementation and Application of Automata
rédacteurs en chef	B Bouchou-Markhoff
Lieu de publication	Heidelberg
Editeur	Springer
Pages	250-263
Nombre de pages	14
Volume	6807
ISBN (imprimé)	9783642222559
Les DOIs	https://doi.org/10.1007/978-3-642-22256-6_23
Etat de la publication	Publié - 2011

Accès au document

10.1007/978-3-642-22256-6_23

Extended version
72050manuscrit soumis, 254 KB

http://www.scopus.com/inward/record.url?partnerID=yv4JPVwI&eid=2-s2.0-79961186165&md5=f02935044ea05c60d3ffcbd0d559e4ff

Model-driven engineering
Cleve, A.
1/01/10 → 31/01/10
Projet: Axe de recherche

Contient cette citation

@inproceedings{855fa8532f6f4fa2a62ccf33a97fe1e8,

title = "Distributed Event Clock Automata: Extended abstract",

abstract = "In distributed real-time systems, we cannot assume that clocks are perfectly synchronized. To model them, we use independent clocks and define their timed semantics. The universal timed language, and the timed language inclusion of icTA are undecidable. Thus, we propose Recursive Distributed Event Clock Automata (DECA). DECA are closed under all boolean operations and their timed language inclusion problem is decidable (more precisely PSPACE-complete), allowing stepwise refinement. We also propose Distributed Event Clock Temporal Logic (DECTL), a real-time logic with independent time evolutions. This logic can be model-checked by translating a DECTL formula into a DECA automaton.",

author = "{Ortiz Vega}, James and Axel Legay and Pierre-Yves Schobbens",

note = "Publication editors : B. Bouchou-Markhoff et al.",

year = "2011",

doi = "10.1007/978-3-642-22256-6_23",

language = "English",

isbn = "9783642222559",

volume = "6807",

pages = "250--263",

editor = "B Bouchou-Markhoff",

booktitle = "CIAA 2011",

publisher = "Springer",

}

Distributed Event Clock Automata: Extended abstract. / Ortiz Vega, James; Legay, Axel; Schobbens, Pierre-Yves.
CIAA 2011: 16th International Conference on Implementation and Application of Automata . Ed. / B Bouchou-Markhoff. Vol 6807 Heidelberg: Springer, 2011. p. 250-263.

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférence › Article dans les actes d'une conférence/un colloque

TY - GEN

T1 - Distributed Event Clock Automata

T2 - Extended abstract

AU - Ortiz Vega, James

AU - Legay, Axel

AU - Schobbens, Pierre-Yves

N1 - Publication editors : B. Bouchou-Markhoff et al.

PY - 2011

Y1 - 2011

N2 - In distributed real-time systems, we cannot assume that clocks are perfectly synchronized. To model them, we use independent clocks and define their timed semantics. The universal timed language, and the timed language inclusion of icTA are undecidable. Thus, we propose Recursive Distributed Event Clock Automata (DECA). DECA are closed under all boolean operations and their timed language inclusion problem is decidable (more precisely PSPACE-complete), allowing stepwise refinement. We also propose Distributed Event Clock Temporal Logic (DECTL), a real-time logic with independent time evolutions. This logic can be model-checked by translating a DECTL formula into a DECA automaton.

AB - In distributed real-time systems, we cannot assume that clocks are perfectly synchronized. To model them, we use independent clocks and define their timed semantics. The universal timed language, and the timed language inclusion of icTA are undecidable. Thus, we propose Recursive Distributed Event Clock Automata (DECA). DECA are closed under all boolean operations and their timed language inclusion problem is decidable (more precisely PSPACE-complete), allowing stepwise refinement. We also propose Distributed Event Clock Temporal Logic (DECTL), a real-time logic with independent time evolutions. This logic can be model-checked by translating a DECTL formula into a DECA automaton.

U2 - 10.1007/978-3-642-22256-6_23

DO - 10.1007/978-3-642-22256-6_23

M3 - Conference contribution

SN - 9783642222559

VL - 6807

SP - 250

EP - 263

BT - CIAA 2011

A2 - Bouchou-Markhoff, B

PB - Springer

CY - Heidelberg

ER -

Distributed Event Clock Automata: Extended abstract

Résumé

Accès au document

Empreinte digitale

Projets

Model-driven engineering

Contient cette citation