Fundamenta Informaticae - Volume 143, issue 3-4

Authors: Abdulla, Parosh Aziz | Demri, Stéphane | Finkel, Alain | Leroux, Jérôme | Potapov, Igor

Article Type: Other

DOI: 10.3233/FI-2016-1311

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. i-ii, 2016

Authors: Akshay, S. | Hélouët, Loïc | Jard, Claude | Reynier, Pierre-Alain

Article Type: Research Article

Abstract: Robustness of timed systems aims at studying whether infinitesimal perturbations in clock values can result in new discrete behaviors. A model is robust if the set of discrete behaviors is preserved under arbitrarily small (but positive) perturbations. We tackle this problem for time Petri nets (TPNs, for short) by considering the model of parametric guard enlargement which allows time-intervals constraining the firing of transitions in TPNs to be enlarged by a (positive) parameter. We show that TPNs are not robust in general and checking if they are robust with respect to standard properties (such as boundedness, safety) is undecidable. …We then extend the marking class timed automaton construction for TPNs to a parametric setting, and prove that it is compatible with guard enlargements. We apply this result to the (undecidable) class of TPNs which are robustly bounded (i.e., whose finite set of reachable markings remains finite under infinitesimal perturbations): we provide two decidable robustly bounded subclasses, and show that one can effectively build a timed automaton which is timed bisimilar even in presence of perturbations. This allows us to apply existing results for timed automata to these TPNs and show further robustness properties. Show more

Keywords: Time Petri nets, Robustness, Timed automata

DOI: 10.3233/FI-2016-1312

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 207-234, 2016

Authors: Bérard, Beatrice | Haddad, Serge | Jovanović, Aleksandra | Lime, Didier

Article Type: Research Article

Abstract: 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. Show more

DOI: 10.3233/FI-2016-1313

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 235-259, 2016

Authors: Brocchi, Stefano | Massazza, Paolo

Article Type: Research Article

Abstract: We consider two new granular dynamical systems obtained from the Sand Pile Model SPM(n ) by adding a smoothness condition. First, we define the Smooth Sand Pile Model SmSPM(n ) and we provide a characterization of the reachable states, together with some interesting properties of the resulting lattice. Then we extend it to SmSPM*(n ), a related dynamical system with a more complex lattice structure.

Keywords: sand piles, discrete dynamical system

DOI: 10.3233/FI-2016-1314

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 261-286, 2016

Authors: Delzanno, Giorgio | Sangnier, Arnaud | Traverso, Riccardo

Article Type: Research Article

Abstract: We study parameterized verification problems for networks of interacting register automata. The network is represented through a graph, and processes may exchange broadcast messages containing data with their neighbours. Upon reception a process can either ignore a sent value, test for equality with a value stored in a register, or simply store the value in a register. We consider safety properties expressed in terms of reachability, from arbitrarily large initial configurations, of a configuration exposing some given control states and patterns. We investigate, in this context, the impact on decidability and complexity of the number of local registers, the number …of values carried by a single message, and dynamic reconfigurations of the underlying network. Show more

DOI: 10.3233/FI-2016-1315

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 287-316, 2016

Authors: Haase, Christoph | Ouaknine, Joël | Worrell, James

Article Type: Research Article

Abstract: We establish a relationship between reachability problems in timed automata and space-bounded counter automata. We show that reachability in timed automata with three or more clocks is logarithmic-space inter-reducible with reachability in space-bounded counter automata with two counters. We moreover show the logarithmic-space equivalence of reachability in two-clock timed automata and space-bounded one-counter automata. This last reduction has recently been employed by Fearnley and Jurdziński to settle the computational complexity of reachability in two-clock timed automata.

Keywords: timed automata, counter automata, reachability, infinite-state systems

DOI: 10.3233/FI-2016-1316

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 317-338, 2016

Authors: Mayr, Richard | Totzke, Patrick

Article Type: Research Article

Abstract: We consider the model checking problem for Gap-order Constraint Systems (GCS) w.r.t. the branching-time temporal logic CTL, and in particular its fragments EG and EF. GCS are nondeterministic infinitely branching processes described by evolutions of integer-valued variables, subject to Presburger constraints of the form x − y ≥ k , where x and y are variables or constants and k ∈ ℕ is a non-negative constant. We show that EG model checking is undecidable for GCS, while EF is decidable. In particular, this implies the decidability of strong and weak bisimulation equivalence between GCS and …finite-state systems. Show more

DOI: 10.3233/FI-2016-1317

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 339-353, 2016

Authors: Mayr, Ernst W. | Weihmann, Jeremias

Article Type: Research Article

Abstract: We investigate gcf-Petri nets, a generalization of communication-free Petri nets allowing arbitrary arc multiplicities, and characterized by the sole restriction that each transition has at most one incoming arc. We use canonical firing sequences with nice properties for gcf-PNs to show that the RecLFS, (zero-)reachability, covering, and boundedness problems of gcf-PNs are in PSPACE . By simulating PSPACE -Turing machines by gss-PNs, a subclass of gcf-PNs where additionally all transitions have at most one outgoing arc, we ultimately obtain PSPACE -completess for these problems in case of gss-PNs or gcf-PNs. Additionally, we prove PSPACE -completeness for the liveness problem of …gcf-PNs. Last, we show PSPACE -hardness as well as a doubly exponential space upper bound for the containment and equivalence problems of gss-PNs or gcf-PNs. Show more

Keywords: Generalized communication-free Petri nets, join-free Petri nets, generalized S-systems, weighted state machines, arbitrary arc multiplicities, arbitrary edge multiplicities, general arc multiplicities, general edge multiplicities, generalized Petri nets, general Petri nets, reachability, boundedness, covering, liveness, equivalence, containment

DOI: 10.3233/FI-2016-1318

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 355-391, 2016

Authors: Piipponen, Artturi | Valmari, Antti

Article Type: Research Article

Abstract: This publication addresses two bottlenecks in the construction of minimal coverability sets of Petri nets: the detection of situations where the marking of a place can be converted to ω , and the manipulation of the set A of maximal ω -markings that have been found so far. For the former, a technique is presented that consumes very little time in addition to what maintaining A consumes. It is based on Tarjan’s algorithm for detecting maximal strongly connected components of a directed graph. For the latter, a data structure is introduced that resembles BDDs and Covering Sharing Trees, …but has additional heuristics designed for the present use. Results from a few experiments are shown. They demonstrate significant savings in running time and varying savings in memory consumption compared to an earlier state-of-the-art technique. Show more

Keywords: coverability set, Tarjan’s algorithm, antichain data structure

DOI: 10.3233/FI-2016-1319

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 393-414, 2016

Authors: Reichert, Julien

Article Type: Research Article

Abstract: Counter reachability games are played by two players on a graph with labelled edges. Each move consists of picking an edge from the current location and adding its label to a counter vector. The objective is to reach a given counter value in a given location. We distinguish three semantics for counter reachability games, according to what happens when a counter value would become negative: the edge is either disabled, or enabled but the counter value becomes zero, or enabled. We consider the problem of determining the winner in counter reachability games and show that, in most cases, it has …the same complexity under all semantics. This constrasts with the one-player case, for which the decision problem is decidable without any elementary upper bound under the first semantics, whereas it is NP-complete under the third one. Surprisingly, under one semantics, the complexity in dimension one depends on whether the objective value is zero or any other integer. Show more

DOI: 10.3233/FI-2016-1320

Citation: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 415-436, 2016