• xmlui.mirage2.page-structure.header.title
    • français
    • English
  • Help
  • Login
  • Language 
    • Français
    • English
View Item 
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Browse

BIRDResearch centres & CollectionsBy Issue DateAuthorsTitlesTypeThis CollectionBy Issue DateAuthorsTitlesType

My Account

LoginRegister

Statistics

Most Popular ItemsStatistics by CountryMost Popular Authors
Thumbnail - Request a copy

Timed substitutions for regular signal-event languages

Bérard, Béatrice; Gastin, Paul; Petit, Antoine (2007), Timed substitutions for regular signal-event languages, Formal Methods in System Design, 31, 2, p. 101-134. http://dx.doi.org/10.1007/s10703-007-0034-5

Type
Article accepté pour publication ou publié
Date
2007
Journal name
Formal Methods in System Design
Volume
31
Number
2
Publisher
Kluwer Academic Publishers
Pages
101-134
Publication identifier
http://dx.doi.org/10.1007/s10703-007-0034-5
Metadata
Show full item record
Author(s)
Bérard, Béatrice
Gastin, Paul
Petit, Antoine
Abstract (EN)
In the classical framework of formal languages, a refinement operation is modeled by a substitution and an abstraction by an inverse substitution. These mechanisms have been widely studied, because they describe a change in the specification level, from an abstract view to a more concrete one, or conversely. For timed systems, there is up to now no uniform notion of substitution. In this paper, we study timed substitutions in the general framework of signal-event languages, where both signals and events are taken into account. We prove that regular signal-event languages are closed under substitution and inverse substitution. To obtain these results, we use in a crucial way a "well known" result: regular signal-event languages are closed under intersection. In fact, while this result is indeed easy for languages defined by Alur and Dill's timed automata, it turns out that the construction is much more tricky when considering the most involved model of signal-event automata. We give here a construction working on finite and infinite signal-event words and taking into account signal stuttering, unobservability of zero-duration τ-signals and Zeno runs. Note that if several constructions have been proposed in particular cases, it is the first time that a general construction is provided.
Subjects / Keywords
Timed automata; Substitution; Signal-event word; Refinement; Abstraction

Related items

Showing items related by title and author.

  • Thumbnail
    Intersection of Regular Signal-Event (Timed) Languages 
    Bérard, Béatrice; Gastin, Paul; Petit, Antoine (2006) Communication / Conférence
  • Thumbnail
    Refinements and Abstractions of Signal-Event (Timed) Languages 
    Petit, Antoine; Gastin, Paul; Bérard, Béatrice (2006) Communication / Conférence
  • Thumbnail
    Timed temporal logics for abstracting transient states 
    Bel Mokadem, Houda; Bérard, Béatrice; Bouyer, Patricia; Laroussinie, François (2006) Communication / Conférence
  • Thumbnail
    A New Modality for Almost Everywhere Properties in Timed Automata 
    Bel Mokadem, Houda; Bérard, Béatrice; Bouyer, Patricia; Laroussinie, François (2005) Communication / Conférence
  • Thumbnail
    Analysing the PGM protocol with Uppaal 
    Petit, Antoine; Bouyer, Patricia; Bérard, Béatrice (2004) Article accepté pour publication ou publié
Dauphine PSL Bibliothèque logo
Place du Maréchal de Lattre de Tassigny 75775 Paris Cedex 16
Phone: 01 44 05 40 94
Contact
Dauphine PSL logoEQUIS logoCreative Commons logo