Author name cluster

B. Bérard

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

I&C Journal 2021 Journal Article

Polynomial interrupt timed automata: Verification and expressiveness

B. Bérard
S. Haddad
C. Picaronny
M. Safey El Din
M. Sassolas

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 are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (PolITA ). We prove that reachability is decidable in 2EXPTIME on PolITA, using an adaptation of the cylindrical algebraic decomposition algorithm for the first-order theory of reals. We also obtain decidability for the model checking of a timed version of CTL and for reachability in several extensions of PolITA. In particular, compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also study expressiveness questions for PolITA and show that PolITA are incomparable with stopwatch automata.

Details DOI

TCS Journal 2013 Journal Article

The expressive power of time Petri nets

B. Bérard
F. Cassez
S. Haddad
D. Lime
O.H. Roux

We investigate expressiveness questions for time Petri nets (TPNs) and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs) as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs. We give a syntactical translation from bounded GTPNs to timed automata (TA) that generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly less expressive than TA w. r. t. weak timed bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally expressive w. r. t. timed language acceptance. Finally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs “à la Merlin” w. r. t. weak timed bisimilarity. These results provide a unified comparison of the expressiveness of many variants of timed models often used in practice. It leads to new important results for TPNs. Among them are: 1-safe TPNs and bounded-TPNs are equally expressive; ε -transitions strictly increase the expressive power of TPNs; self modifying nets as well as read, inhibitor and reset arcs do not add expressiveness to bounded TPNs.

Details DOI

TCS Journal 2008 Journal Article

When are Timed Automata weakly timed bisimilar to Time Petri Nets?

B. Bérard
F. Cassez
S. Haddad
D. Lime
O.H. Roux

In this paper, we compare Timed Automata (TA) and Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is strictly included in the class of TA. It is thus natural to try and identify the subclass T A w t b of TA equivalent to some TPN for the weak timed bisimulation relation. We give a characterization of this subclass and we show that the membership problem and the reachability problem for T A w t b are P S P A C E -complete. Furthermore we show that for a TA in T A w t b with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w. r. t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.

Details DOI