Fundamenta Informaticae - Volume 178, issue 1-2

Authors: Hague, Matthew | Potapov, Igor

Article Type: Other

DOI: 10.3233/FI-2021-1995

Citation: Fundamenta Informaticae, vol. 178, no. 1-2, pp. v-vi, 2021

Authors: Bruse, Florian | Lange, Martin | Lozes, Etienne

Article Type: Research Article

Abstract: Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ -calculus into the modal μ -calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k -EXPTIME-complete for formulas that use functions of type order at most k < 0. In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in (k − 1)-EXPSPACE, and …also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL. Show more

DOI: 10.3233/FI-2021-1996

Citation: Fundamenta Informaticae, vol. 178, no. 1-2, pp. 1-30, 2021

Authors: Cassez, Franck | Jensen, Peter Gjøl | Guldstrand Larsen, Kim

Article Type: Research Article

Abstract: We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to …state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools. Show more

DOI: 10.3233/FI-2021-1997

Citation: Fundamenta Informaticae, vol. 178, no. 1-2, pp. 31-57, 2021

Authors: Filiot, Emmanuel | Reynier, Pierre-Alain

Article Type: Research Article

Abstract: Copyless streaming string transducers (copyless SST) have been introduced by R. Alur and P. Černý in 2010 as a one-way deterministic automata model to define transductions of finite strings. Copyless SST extend deterministic finite state automata with a set of variables in which to store intermediate output strings, and those variables can be combined and updated all along the run, in a linear manner, i.e., no variable content can be copied on transitions. It is known that copyless SST capture exactly the class of MSO-definable string-to-string transductions, and are as expressive as deterministic two-way transducers. They enjoy good algorithmic properties. …Most notably, they have decidable equivalence problem (in PSpace ). On the other hand, HDT0L systems have been introduced for a while, the most prominent result being the decidability of the equivalence problem. In this paper, we propose a semantics of HDT0L systems in terms of transductions, and use it to study the class of deterministic copyful SST. Our contributions are as follows:(i) HDT0L systems and total deterministic copyful SST have the same expressive power, (ii) the equivalence problem for deterministic copyful SST and the equivalence problem for HDT0L systems are inter-reducible, in quadratic time. As a consequence, equivalence of deterministic SST is decidable, (iii) the functionality of non-deterministic copyful SST is decidable, (iv) determining whether a non-deterministic copyful SST can be transformed into an equivalent non-deterministic copyless SST is decidable in polynomial time. HDT0L systems and total deterministic copyful SST have the same expressive power, the equivalence problem for deterministic copyful SST and the equivalence problem for HDT0L systems are inter-reducible, in quadratic time. As a consequence, equivalence of deterministic SST is decidable, the functionality of non-deterministic copyful SST is decidable, determining whether a non-deterministic copyful SST can be transformed into an equivalent non-deterministic copyless SST is decidable in polynomial time. Show more

Keywords: words, transducers, equivalence problem

DOI: 10.3233/FI-2021-1998

Citation: Fundamenta Informaticae, vol. 178, no. 1-2, pp. 59-76, 2021

Authors: Hutagalung, Milka

Article Type: Research Article

Abstract: Multi-buffer simulation is an extension of simulation preorder that can be used to approximate inclusion of languages recognised by Büchi automata up to their trace closures. DUPLICATOR can use some bounded or unbounded buffers to simulate SPOILER ’s move. It has been shown that multi-buffer simulation can be characterised with the existence of a continuous function. In this paper, we show that such a characterisation can be refined to a more restricted case, that is, to the one where DUPLICATOR only uses bounded buffers, by requiring the function to be Lipschitz continuous instead of only continuous. This characterisation …however only holds for some restricted classes of automata. One of the automata should only produce words where each letter cannot commute unboundedly. We show that this property can be syntactically characterised with cyclic-path-connectedness, a refinement of syntactic condition on automata that have regular trace closure. We further show that checking cyclic-path-connectedness is indeed co-NP-complete. Show more

DOI: 10.3233/FI-2021-1999

Citation: Fundamenta Informaticae, vol. 178, no. 1-2, pp. 77-99, 2021

Authors: Sproston, Jeremy

Article Type: Research Article

Abstract: Probabilistic timed automata are classical timed automata extended with discrete probability distributions over edges. We introduce clock-dependent probabilistic timed automata, a variant of probabilistic timed automata in which transition probabilities can depend linearly on clock values. Clock-dependent probabilistic timed automata allow the modelling of a continuous relationship between time passage and the likelihood of system events. We show that the problem of deciding whether the maximum probability of reaching a certain location is above a threshold is undecidable for clock-dependent probabilistic timed automata. On the positive side, we show that the maximum and minimum probability of reaching a certain location …in clock-dependent probabilistic timed automata can be approximated using a region-graph-based approach. Show more

Keywords: Probabilistic model checking, timed automata

DOI: 10.3233/FI-2021-2000

Citation: Fundamenta Informaticae, vol. 178, no. 1-2, pp. 101-138, 2021

Authors: Valmari, Antti | Vogler, Walter

Article Type: Research Article

Abstract: Many partial order methods use some special condition for ensuring that the analysis is not terminated prematurely. In the case of stubborn set methods for safety properties, implementation of the condition is usually based on recognizing the terminal strong components of the reduced state space and, if necessary, expanding the stubborn sets used in their roots. In an earlier study it was pointed out that if the system may execute a cycle consisting of only invisible actions and that cycle is concurrent with the rest of the system in a non-obvious way, then the method may be fooled to construct …all states of the full parallel composition. This problem is solved in this study by a method that “freezes” the actions in the cycle. The new method also preserves fair testing equivalence, making it usable for the verification of many progress properties. Show more

Keywords: partial order methods, stubborn sets, safety properties, ignoring problem, fair testing

DOI: 10.3233/FI-2021-2001

Citation: Fundamenta Informaticae, vol. 178, no. 1-2, pp. 139-172, 2021