International Journal of Foundations of Computer Science

We introduce the simple and efficient method of monotonic abstraction to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables over finite domains. The method of monotonic abstraction derives an over-approximation of the induced transition system that allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype that works well on several mutual exclusion algorithms and cache coherence protocols.

The goal of this presentation is to analyze the equality mechanism of cooperating morphisms of free monoids, and to point out how it can be used to define the reachability problems leading to important undecidability results and easy characterizations of recursively enumerable languages. In particular, we aim to show, which subconstructions are needed in such results. Moreover, we recall that in some cases the undecidability of the reachability is achieved although the sets of all reachable objects are simple, or more formally, regular languages.

We consider in this paper systems modeled by timed automata. The timing bounds involved in the action guards and location invariants of our timed automata are not constants, but parameters. Those parametric timed automata allow the modelling of various kinds of timed systems, e.g. communication protocols or asynchronous circuits. We will also assume that we are given an initial tuple π₀ of values for the parameters, which corresponds to values for which the system is known to behave properly. Our goal is to compute a constraint K₀ on the parameters, satisfied by π₀, guaranteeing that, under any parameter valuation satisfying K₀, the system behaves in the same manner: for any two parameter valuations satisfying K₀, the behaviors of the timed automata are (time-abstract) equivalent, i.e., the traces of execution viewed as alternating sequences of actions and locations are identical. We present an algorithm InverseMethod that terminates in the case of acyclic models, and discuss how to extend it to the cyclic case. We also explain how to combine our method with classical synthesis methods which are based on the avoidance of a given set of bad states. A prototype implementation has been done, and various experiments are described.

This paper addresses the following general problem of tree regular model-checking: decide whether where is the reflexive and transitive closure of a successor relation induced by a term rewriting system , and and are both regular tree languages. We develop an automatic approximation-based technique to handle this – undecidable in general – problem in the case when term rewriting system rules are non left-linear.

In model-checking the systems under investigation often arise in the form of products. The compositional method, developed by Feferman and Vaught in 1959, fits to this situation and can be used to deduce the truth of a formula in the product from information in the factors. Building on earlier work of Wöhrle and Thomas (2004), we study first-order logic with reachability predicates over finitely synchronized products (i.e. synchronized products with a finite number of synchronization transitions). We extend the reachability predicates by conditions on the length of the corresponding paths, formulated in Presburger arithmetic. For finitely synchronized products with these enhanced reachability predicates we prove a composition theorem and then show that severe limitations exist for generalisations of this result.

Switching graphs are graphs that contain switches. A switch is a pair of edges that start in the same vertex and of which precisely one edge is enabled at any time. By using a Boolean function called a switch setting, the switches in a switching graph can be put in a fixed direction to obtain an ordinary graph. For many problems, switching graphs are a remarkable straightforward and natural model, but they have hardly been studied. We study the complexity of several natural questions in switching graphs of which some are polynomial, and others are NP-complete. We started investigating switching graphs because they turned out to be a natural framework for studying the problem of solving Boolean equation systems, which is equivalent to model checking of the modal µ-calculus and deciding the winner in parity games. We give direct, polynomial encodings of Boolean equation systems in switching graphs and vice versa, and prove correctness of the encodings.

We study subset reachability in nondeterministic finite automata and look for bounds of the length of the shortest reaching words for automata with a fixed number of states. We obtain such bounds for nondeterministic automata over 2-letter, 3-letter and arbitrary alphabets.^a

The satisfiability problems for and are known to be EXPTIME-complete, resp. 2EXPTIME-complete (Fischer and Ladner (1979), Vardi and Stockmeyer (1985)). For fragments that use less temporal or propositional operators, the complexity may decrease. This paper undertakes a systematic study of satisfiability for -and -formulae over restricted sets of propositional and temporal operators. We show that restricting the temporal operators yields satisfiability problems complete for 2EXPTIME, EXPTIME, PSPACE, and NP. Restricting the propositional operators either does not change the complexity (as determined by the temporal operators), or yields very low complexity like NC¹, TC⁰, or NLOGTIME.

A pure morphic sequence is a right-infinite, symbolic sequence obtained by iterating a letter-to-word substitution. For instance, the Fibonacci sequence and the Thue–Morse sequence, which play an important role in theoretical computer science, are pure morphic. Define a coding as a letter-to-letter substitution. The image of a pure morphic sequence under a coding is called a morphic sequence.

A sequence x is called uniformly recurrent if for each finite subword u of x there exists an integer l such that u occurs in every l-length subword of x.

The paper mainly focuses on the problem of deciding whether a given morphic sequence is uniformly recurrent. Although the status of the problem remains open, we show some evidence for its decidability: in particular, we prove that it can be solved in polynomial time on pure morphic sequences and on automatic sequences.

In addition, we prove that the complexity of every uniformly recurrent, morphic sequence has at most linear growth: here, complexity is understood as the function that maps each positive integer n to the number of distinct n-length subwords occurring in the sequence.

Homogeneous multiprocessor systems are usually modelled by undirected graphs. Vertices of these graphs represent the processors, while edges denote the connection links between adjacent processors. Let G be a graph with diameter D, maximum vertex degree Δ, the largest eigenvalue λ₁ and m distinct eigenvalues. The products mΔ and (D+1)λ₁ are called the tightness of G of the first and second type, respectively. In recent literature it was suggested that graphs with a small tightness of the first type are good models for the multiprocessor interconnection networks. In a previous paper we studied these and some other types of tightness and some related graph invariants and demonstrated their usefulness in the analysis of multiprocessor interconnection networks. We proved that the number of connected graphs with a bounded tightness is finite. In this paper we determine explicitly graphs with tightness values not exceeding 9. There are 69 such graphs and they contain up to 10 vertices. In addition we identify graphs with minimal tightness values when the number of vertices is n = 2,…, 10.