22 citations · 30 across the 5 of their papers we have counts for
5 papers
Polynomial Interrupt Timed Automata
Béatrice Bérard, Serge Haddad, Claudine Picaronny +2
Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They…
Interrupt Timed Automata with Auxiliary Clocks and Parameters
Béatrice Bérard, Serge Haddad, Aleksandra Jovanović +1
Interrupt Timed Automata (ITA) is an expressive timed model, introduced to take into account interruptions, according to levels. Due to this feature, this formalism is incomparable…
Verification of Information Flow Properties under Rational Observation
Béatrice Bérard, John Mullins
Information flow properties express the capability for an agent to infer information about secret behaviours of a partially observable system. In a language-theoretic setting, wher…
Probabilistic Opacity for Markov Decision Processes
Béatrice Bérard, Krishnendu Chatterjee, Nathalie Sznajder
Opacity is a generic security property, that has been defined on (non probabilistic) transition systems and later on Markov chains with labels. For a secret predicate, given as a s…
Interrupt Timed Automata: verification and expressiveness
Béatrice Bérard, Serge Haddad, Mathieu Sassolas
We introduce the class of Interrupt Timed Automata (ITA), a subclass of hybrid automata well suited to the description of timed multi-task systems with interruptions in a single pr…