Wyniki wyszukiwania - BazTech

1

Interrupt Timed Automata with Auxiliary Clocks and Parameters

Bérard B., Jovanović A., Haddad S., Lime D.

Fundamenta Informaticae

|

2016

|

Vol. 143, nr 3/4

235--259

EN

Interrupt Timed Automata (ITA) are an expressive timed model, introduced to take into account interruptions according to levels. Due to this feature, this formalism is incomparable with Timed Automata. However several decidability results related to reachability and model checking have been obtained. We add auxiliary clocks to ITA, thereby extending its expressive power while preserving decidability of reachability. Moreover, we define a parametrized version of ITA, with polynomials of parameters appearing in guards and updates. While parametric reasoning is particularly relevant for timed models, it very often leads to undecidability results. We prove that various reachability problems, including robust reachability, are decidable for this model, and we give complexity upper bounds for a fixed or variable number of clocks, levels and parameters.

2

Complexity Analysis of Continuous Petri Nets

Fraca E., Haddad S.

Fundamenta Informaticae

|

2015

|

Vol. 137, nr 1

1--28

EN

At the end of the eighties, continuous Petri nets were introduced for: (1) alleviating the combinatory explosion triggered by discrete Petri nets (i.e. usual Petri nets) and, (2) modelling the behaviour of physical systems whose state is composed of continuous variables. Since then several works have established that the computational complexity of deciding some standard behavioural properties of Petri nets is reduced in this framework. Here we first establish the decidability of additional properties like coverability, boundedness and reachability set inclusion. We also design new decision procedures for reachability and lim-reachability problems with a better computational complexity. Finally we provide lower bounds characterising the exact complexity class of the reachability, the coverability, the boundedness, the deadlock freeness and the liveness problems. A small case study is introduced and analysed with these new procedures.

3

Synthesis and Analysis of Product-form Petri Nets

Haddad S., Mairesse J., Nguyen H. T.

Fundamenta Informaticae

|

2013

|

Vol. 122, nr 1-2

147--172

EN

For a large Markovian model, a "product form" is an explicit description of the steadystate behaviour which is otherwise generally untractable. Being first introduced in queueing networks, it has been adapted to Markovian Petri nets. Here we address three relevant issues for product-form Petri nets which were left fully or partially open: (1) we provide a sound and complete set of rules for the synthesis; (2) we characterise the exact complexity of classical problems like reachability; (3) we introduce a new subclass for which the normalising constant (a crucial value for product-form expression) can be efficiently computed.

4

Undecidability Results for Timed Automata with Silent Transitions

Bouyer P., Haddad S., Reynier P-A.

Fundamenta Informaticae

|

2009

|

Vol. 92, nr 1-2

1-25

EN

In this work, we study decision problems related to timed automata with silent transitions (TAε) which strictly extend the expressiveness of timed automata (TA). We first answer negatively a central question raised by the introduction of silent transitions: can we decide whether the language recognized by a TAε can be recognized by some TA? Then we establish in the framework of TAε some old open conjectures that O. Finkel has recently solved for TA. His proofs follow a generic scheme which relies on the fact that only a finite number of configurations can be reached by a TA while reading a timed word. This property does not hold for TAε , the proofs in the framework of TAε thus require more elaborated arguments. We establish undecidability of complementability, minimization of the number of clocks, and closure under shuffle. We also show these results in the framework of infinite timed languages.