Search

The problem of uniformly placing N points onto a sphere finds applications in many areas. For example, points on the sphere correspond to unit quaternions as well as to the group of rotations SO(3) and the online version of generating uniform rotations (known as "incremental generation") plays a crucial role in a large number of engineering applications ranging from robotics and aeronautics to computer graphics. An online version of this problem was recently studied with respect to the gap ratio as a measure of uniformity. The first online algorithm of Chen et al. was upper-bounded by 5.99 and later improved to 3.69, which is achieved by considering a circumscribed dodecahedron followed by a recursive decomposition of each face. In this paper we provide a more efficient tessellation technique based on the regular icosahedron, which improves the upper-bound for the online version of this problem, decreasing it to approximately 2.84. Moreover, we show that the lower bound for the gap ratio of placing at least three points is (1 + 5) / 2 ≈ 1.618 and for at least four points is no less than 1.726. [ABSTRACT FROM AUTHOR]

Abstract This paper solves three open problems about the decidability of the vector and scalar reachability problems and the point to point reachability by fractional linear transformations over finitely generated semigroups of matrices from SL (2 , Z). Our approach to solving these problems is based on the characterization of reachability paths between vectors or points, which is then used to translate the numerical problems on matrices into computational problems on words and regular languages. We will also give geometric interpretations of these results. Highlights • The vector reachability problem in SL (2 , Z) is decidable. • The scalar reachability problem in SL (2 , Z) is decidable. • Reachability problem by fractional linear transformations in SL (2 , Z) is decidable. • Proofs are based on translating matrix equations into problems on regular languages. • We give a geometric interpretation and prove generalizations of these results. [ABSTRACT FROM AUTHOR]

We study the vector ambiguity problem and the vector freeness problem in SL(2,Z). Given a finitely generated n x n matrix semigroup S and an n-dimensional vector x, the vector ambiguity problem is to decide whether for every target vector y = Mx, where M ∈ S, M is unique. We also consider the vector freeness problem which is to show that every matrix M which is transforming x to Mx has a unique factorization with respect to the generator of S. We show that both problems are NP-complete in SL(2,Z), which is the set of 2 x 2 integer matrices with determinant 1. Moreover, we generalize the vector ambiguity problem and extend to the finite and k-vector ambiguity problems where we consider the degree of vector ambiguity of matrix semigroups. [ABSTRACT FROM AUTHOR]

A temporal graph is a dynamic graph where every edge is assigned a set of integer time labels that indicate at which discrete time step the edge is available. In this paper, we study how changes of the time labels, corresponding to delays on the availability of the edges, affect the reachability sets from given sources. We introduce control mechanisms for reachability sets that are based on two natural operations of delaying. The first operation, termed merging, is global and batches together consecutive time labels into a single time label in the whole network simultaneously. The second, imposes independent delays on the time labels of every edge of the graph. We provide a thorough investigation of the computational complexity of different objectives related to reachability sets when these operations are used. [ABSTRACT FROM AUTHOR]

We consider a variant of the mortality problem: given k × k matrices A 1 , ... , A t , do there exist nonnegative integers m 1 , ... , m t such that A 1 m 1 ⋯ A t m t equals the zero matrix? This problem is known to be decidable when t ≤ 2 but undecidable for integer matrices with sufficiently large t and k. We prove that for t = 3 this problem is Turing-equivalent to Skolem's problem and thus decidable for k ≤ 3 (resp. k = 4) over (resp. real) algebraic numbers. Consequently, the set of triples (m 1 , m 2 , m 3) for which the equation A 1 m 1 A 2 m 2 A 3 m 3 equals the zero matrix is a finite union of direct products of semilinear sets. For t = 4 we show that the solution set can be non-semilinear, and thus there is unlikely to be a connection to Skolem's problem. We prove decidability for upper-triangular 2 × 2 rational matrices by employing powerful tools from transcendence theory such as Baker's theorem and S-unit equations. [ABSTRACT FROM AUTHOR]

We consider a discrete system of n simple indistinguishable devices, called agents , forming a connected shape S I on a two-dimensional square grid. Agents are equipped with a linear-strength mechanism, called a line move , by which an agent can push a whole line of consecutive agents in one of the four cardinal directions in a single time-step. We study the problem of transforming an initial shape S I into a given target shape S F via a finite sequence of line moves in a distributed model, where each agent can observe the states of nearby agents in a Moore neighbourhood. We develop the first distributed connectivity-preserving transformation that exploits line moves. The transformation solves the line formation problem. That is, starting from any shape S I whose associated graph contains a Hamiltonian path known to them, the agents can form a final straight line S L. The complexity of the transformation is O (n log 2 ⁡ n) moves, which is asymptotically equivalent to that of the best-known centralised transformations. • We study a linear-strength model for programmable matter and mobile robotic systems • A single mechanical operation, line pushing, is allowed for the shape formation • A distributed algorithmic framework is presented for line moves • The first distributed connectivity-preserving transformation that exploits line moves • Achieve running time equivalent to that of the best-known centralised algorithms [ABSTRACT FROM AUTHOR]

We study a model of programmable matter systems consisting of n devices lying on a 2-dimensional square grid which are able to perform the minimal mechanical operation of rotating around each other. The goal is to transform an initial shape A into a target shape B. We investigate the class of shapes which can be constructed in such a scenario under the additional constraint of maintaining global connectivity at all times. We focus on the scenario of transforming nice shapes , a class of shapes consisting of a central line L where for all nodes u in S either u ∈ L or u is connected to L by a line of nodes perpendicular to L. We prove that by introducing a minimal 3-node seed it is possible for the canonical shape of a line of n nodes to be transformed into a nice shape of n − 1 nodes. We use this to show that a 4-node seed enables the transformation of nice shapes of size n into any other nice shape of size n in O (n 2) time. We leave as an open problem the expansion of the class of shapes which can be constructed using such a seed to include those derived from nice shapes. • We study theoretical models of programmable matter systems. • One minimal mechanical operation is allowed: rotation. • Focus on transformability questions: can a given shape be transformed into another? • With the help of three additional nodes can convert a line of nodes into any nice shape with constant waste. • With the help of four additional nodes can convert a nice shape into any other nice shape via the line without waste. [ABSTRACT FROM AUTHOR]

Abstract: In this paper, we introduce and study an algebra of languages representable by vertex-labeled graphs. The proposed algebra is equipped with three operations: the union of languages, the merging of languages and the iteration. In contrast to Kleene algebra, which is mainly used for edge-labeled graphs, it can adequately represent many properties of languages defined by vertex-labeled graphs and provides a natural translation from vertex-labeled graphs to regular expressions and vice versa. [Copyright &y& Elsevier]

Most computational problems for matrix semigroups and groups are inherently difficult to solve and even undecidable starting from dimension three. The questions about the decidability and complexity of problems for two-dimensional matrix semigroups remain open and are directly linked with other challenging problems in the field. In this paper we study the computational complexity of the problem of determining whether the identity matrix belongs to a matrix semigroup (the Identity Problem) generated by a finite set of 2 × 2 integral unimodular matrices. The Identity Problem for matrix semigroups is a well-known challenging problem, which has remained open in any dimension until recently. It is currently known that the problem is decidable in dimension two and undecidable starting from dimension four. In particular, we show that the Identity Problem for 2 × 2 integral unimodular matrices is NP-hard by a reduction of the Subset Sum Problem and several new encoding techniques. An upper bound for the nontrivial decidability result by C. Choffrut and J. Karhumäki is unknown. However, we derive a lower bound on the minimum length solution to the Identity Problem for a constructible set of instances, which is exponential in the number of matrices of the generator set and the maximal element of the matrices. This shows that the most obvious candidate for an NP algorithm, which is to guess the shortest sequence of matrices which multiply to give the identity matrix, does not work correctly since the certificate would have a length which is exponential in the size of the instance. Both results lead to a number of corollaries confirming the same bounds for vector reachability, scalar reachability and zero in the right upper corner problems. [ABSTRACT FROM AUTHOR]

No abstract received. [ABSTRACT FROM AUTHOR]

In this paper we study several closely related fundamental problems for words and matrices. First, we introduce the Identity Correspondence Problem (ICP): whether a finite set of pairs of words (over a group alphabet) can generate an identity pair by a sequence of concatenations. We prove that ICP is undecidable by a reduction of Post's Correspondence Problem via several new encoding techniques. In the second part of the paper we use ICP to answer a long standing open problem concerning matrix semigroups: "Is it decidable for a finitely generated semigroup S of integral square matrices whether or not the identity matrix belongs to S?". We show that the problem is undecidable starting from dimension four even when the number of matrices in the generator is 48. From this fact, we can immediately derive that the fundamental problem of whether a finite set of matrices generates a group is also undecidable. We also answer several questions for matrices over different number fields. Apart from the application to matrix problems, we believe that the Identity Correspondence Problem will also be useful in identifying new areas of undecidable problems in abstract algebra, computational questions in logic and combinatorics on words. [ABSTRACT FROM AUTHOR]

Abstract: In this paper, we investigate various decision problems concerning parameterized versions of some classes of machines. Let be the class of nondeterministic multitape Turing machine (TM) acceptors with a two-way read-only input, at most states, at most read–write worktapes, and at most symbols in the worktape alphabet, where are fixed positive integers. There is no restriction on the cardinality of the input alphabet. We are able to show the emptiness, disjointness, and universe (also called universality) problems to be decidable for . For the class consisting of machines in that always halt or whose minimal-time accepting computations can be bounded by some recursive function (where is the input length), the containment and equivalence problems are decidable. These results hold for other machines, e.g., when the worktapes are pushdown stacks (where on every step, each pushdown can only pop the top of the stack or replace the top of the stack by at most two symbols) or when stacks are counters (where on every step, a counter can be incremented by 1, decremented by 1, or remain unchanged, and can be tested for zero). Our results are the best possible in the sense that not parameterizing one of (or, in the case of counter machines, allowing the counters to increment by arbitrary integers that may change from machines to machines) makes the universe problem undecidable. We also give a simple characterization of the languages defined by . Finally, we investigate the applicability of our techniques to machines with multiple input heads or multiple input tapes. [Copyright &y& Elsevier]

Querying its own history is an important mechanism in the computations, especially those interacting with people or other computations such as transaction processing, electronic data interchange. John McCarthy in his Elephant programming language proposal suggested exploiting the referring to the past as the main programming primitive. In this paper we study the computational power of such primitive. In order to do that we propose a refined formal model, History Dependent Machine (HDM), which uses querying the history as its sole computational primitive. Our main result may be spelled in general terms as: a model with a single agent wandering around a pool of resources and having ability to check its own history for simple temporal properties has a universal computational power. Moreover, HDM can simulate any multicounter machine in real time. Then we show that the computations of HDM may be specified in the extension of propositional linear temporal logic by flexible constants, the abstraction operator and equality. We use then universality of HDM model to show that the above extension with a single flexible constant is not recursively axiomatizable. [ABSTRACT FROM AUTHOR]

Abstract: We examine computational problems on quaternion matrix and rotation semigroups. It is shown that in the ultimate case of quaternion matrices, in which multiplication is still associative, most of the decision problems for matrix semigroups are undecidable in dimension two. The geometric interpretation of matrix problems over quaternions is presented in terms of rotation problems for the 2- and 3-sphere. In particular, we show that the reachability of the rotation problem is undecidable on the 3-sphere and other rotation problems can be formulated as matrix problems over complex and hypercomplex numbers. [Copyright &y& Elsevier]

In this paper we analyze the dynamics of one-dimensional piecewise maps. We show that one-dimensional piecewise affine maps are equivalent to pseudo-billiard or so called “strange billiard” systems. We also show that use of more general classes of functions lead to undecidability of reachability problem for one-dimensional piecewise maps. [ABSTRACT FROM AUTHOR]

Abstract: In this paper we consider several reachability problems such as vector reachability, membership in matrix semigroups and reachability problems in piecewise linear maps. Since all of these questions are undecidable in general, we work on lowering the bounds for undecidability. In particular, we show an elementary proof of undecidability of the reachability problem for a set of 5 two-dimensional affine transformations. Then, using a modified version of a standard technique, we also prove that the vector reachability problem is undecidable for two (rational) matrices in dimension 11. The above result can be used to show that the system of piecewise linear functions of dimension 12 with only two intervals has an undecidable set-to-point reachability problem. We also show that the “zero in the upper right corner” problem is undecidable for two integral matrices of dimension 18 lowering the bound from 23. [Copyright &y& Elsevier]

In this paper we study the gossiping problem (all-to-all communication) in radio networks where all nodes are aware of the network topology. We start our presentation with a deterministic gossiping algorithm that works in at most units of time in any radio network of size . This algorithm is optimal in the worst case scenario since there exist radio network topologies, such as lines, stars and complete graphs in which radio gossiping cannot be completed in less than communication rounds. Furthermore, we show that there does not exist any radio network topology in which the gossiping task can be solved in less than rounds. We also show that this lower bound can be matched from above for a fraction of all possible integer values of , and for all other values of we propose a solution which accomplishes gossiping in rounds. Then we show an almost optimal radio gossiping algorithm in trees, which misses the optimal time complexity by a single round. Finally, we study asymptotically optimal -time gossiping (where is the diameter of the network) in graphs with the maximum degree , for any integer constant and large enough. [Copyright &y& Elsevier]

Abstract: In this paper, we consider decidability questions that are related to the membership problem in matrix semigroups. In particular, we consider the membership of a given invertible diagonal matrix in a matrix semigroup and then a scalar matrix, which has a separate geometric interpretation. Both problems have been open for any dimensions and are shown to be undecidable in dimension 4 with integral matrices by a reduction of the Post Correspondence Problem (PCP). Although the idea of PCP reduction is standard for such problems, we suggest a new coding technique to cover the case of diagonal matrices. [Copyright &y& Elsevier]

No abstract received. [ABSTRACT FROM AUTHOR]

No abstract received. [ABSTRACT FROM AUTHOR]

We consider a discrete system of n devices lying on a 2-dimensional square grid and forming an initial connected shape S I. Each device is equipped with a linear-strength mechanism which enables it to move a whole line of consecutive devices in a single time-step, called a line move. We study the problem of transforming S I into a given connected target shape S F of the same number of devices, via a finite sequence of line moves. Our focus is on designing centralised transformations aiming at minimising the total number of moves subject to the constraint of preserving connectivity of the shape throughout the course of the transformation. We first give very fast connectivity-preserving transformations for the case in which the associated graphs of S I and S F contain a Hamiltonian path. In particular, our transformations make O (n log ⁡ n) moves, which is asymptotically equal to the best known running time of connectivity-breaking transformations. Our most general result is then a connectivity-preserving universal transformation that can transform any initial connected shape S I into any target connected shape S F , through a sequence of O (n n) moves. [ABSTRACT FROM AUTHOR]

We show that the problem of determining if the identity matrix belongs to a finitely generated semigroup of 2 × 2 matrices from the General Linear Group GL 2 (Z) is solvable in NP. We extend this to prove that the membership problem is decidable in NP for GL 2 (Z) and for any arbitrary regular expression over matrices from the Special Linear group SL 2 (Z). We show that determining if a given finite set of matrices from SL 2 (Z) or the modular group PSL 2 (Z) generates a group or a free semigroup are decidable in NP. Previous algorithms, shown in 2005 by Choffrut and Karhumäki, were in EXPSPACE. Our algorithm is based on new techniques allowing us to operate on compressed word representations of matrices without explicit expansions. When combined with known NP -hard lower bounds, this proves that the membership problem over GL 2 (Z) is NP -complete, and the group problem and the non-freeness problem in SL 2 (Z) are NP -complete. 1 [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

In this work, we study a discrete system of entities residing on a two-dimensional square grid. Each entity is modelled as a node occupying a distinct cell of the grid. The set of all n nodes forms initially a connected shape A. Entities are equipped with a linear-strength pushing mechanism that can push a whole line of entities in parallel in a single time-step on one position in a given (one of the four possible) direction of a grid. A target connected shape B is also provided and the goal is to transform A into B via a sequence of line moves. Existing models based on local movement of individual nodes, such as rotating or sliding a single node, can be shown to be special cases of the present model, therefore their (inefficient, Θ (n 2) -time) universal transformations carry over. Our main goal is to investigate whether the parallelism inherent in this new type of movement can be exploited for efficient, i.e., sub-quadratic worst-case, transformations. This paper provides several solutions for specific and universal centralised transformations in the context of the new model. In particular we first design O (n log ⁡ n) -time universal transformation without preserving the connectivity of original shape. Then we focus on transformations which preserve the connectivity of the shape throughout its course and develop an O (n n) -time transformation for the apparently hard instance of transforming a diagonal A into a straight line B. [ABSTRACT FROM AUTHOR]

Piecewise affine maps (PAMs) are frequently used as a reference model to discuss the frontier between known and open questions about the decidability for reachability questions. In particular, the reachability problem for one-dimensional PAM is still an open problem, even if restricted to only two intervals. As the main contribution of this paper we introduce new techniques for solving reachability problems based on p-adic norms and weights as well as showing decidability for two classes of maps. Then we show the connections between topological properties for PAM’s orbits, reachability problems and representation of numbers in a rational base system. Finally we construct an example where the distribution properties of well studied sequences can be significantly disrupted by taking fractional parts after regular shifts. The study of such sequences could help with understanding similar sequences generated in PAMs or in well known Mahler’s 3/2 problem. [ABSTRACT FROM AUTHOR]

In this paper we combine two classical generalisations of finite automata (weighted automata and automata on infinite words) into a model of integer weighted automata on infinite words and study the universality and the emptiness problems under zero weight acceptance. We show that the universality problem is undecidable for three-state automata by a direct reduction from the infinite Post correspondence problem. We also consider other more general acceptance conditions as well as their complements with respect to the universality and the emptiness problems. Additionally, we build a universal integer weighted automaton with fixed transitions. This automaton has an additional integer input that allows it to simulate any semi-Thue system. [ABSTRACT FROM AUTHOR]

In this paper we introduce and apply a novel approach for self-organisation, partitioning and pattern formation on the non-oriented grid environment. The method is based on the generation of nodal patterns in the environment via sequences of discrete waves. The power of the primitives is illustrated by giving solutions to two geometric problems using the broadcast automata model arranged in an integer grid (a square lattice) formation. In this model automata cannot directly observe their neighbours' state and can only communicate with neighbouring automata through the non-oriented broadcast of messages from a finite alphabet. In particular we show linear time algorithms for the problem of finding the centre of a digital disk starting from any point on the border of the disc and the problem of electing a set of automata that form the inscribed square of such a digital disk. Possible generalizations and applications of techniques based on nodal patterns and the construction of different discrete wave interference pictures are discussed in the conclusion. [ABSTRACT FROM AUTHOR]

Dynamic networks of Pushdown Systems (DNPS in short) have been introduced to perform static analysis of concurrent programs that may spawn threads dynamically. In this model the set of successors of a regular set of configurations can be non-regular, making forward analysis of these models difficult. We refine the model by adding the associative-commutative properties of parallel composition, and we define Presburger weighted tree automata, an extension of weighted automata and tree automata, that accept the set of successors of a regular set of configurations. This yields decidability of the forward analysis of DNPS. Finally, we extend this result to the model where configurations are sets of threads running in parallel. [ABSTRACT FROM AUTHOR]

Abstract: We study here a problem of finding all maximal repetitions in a string of length . We show that the problem can be solved in time in the presence of constant extra space and general (unbounded) alphabets. Subsequently we show that in the model with a constant size alphabet the problem can be solved in time with a help of extra space. Previously best known algorithms require linear additional space in both models. [Copyright &y& Elsevier]

Crystal Structure Prediction (CSP) is one of the central and most challenging problems in materials science and computational chemistry. In CSP, the goal is to find a configuration of ions in 3D space that yields the lowest potential energy. Finding an efficient procedure to solve this complex optimisation question is a well known open problem. Due to the exponentially large search space, the problem has been referred in several materials-science papers as "NP-Hard and very challenging" without a formal proof. This paper fills a gap in the literature providing the first set of formally proven NP-Hardness results for a variant of CSP with various realistic constraints. In particular, we focus on the problem of removal: the goal is to find a substructure with minimal potential energy, by removing a subset of the ions. Our main contributions are NP-Hardness results for the CSP removal problem, new embeddings of combinatorial graph problems into geometrical settings, and a more systematic exploration of the energy function to reveal the complexity of CSP. In a wider context, our results contribute to the analysis of computational problems for weighted graphs embedded into the three-dimensional Euclidean space. [ABSTRACT FROM AUTHOR]

An exact pattern matching problem is to find all occurrences of a pattern p in a text t. We say that the pattern matching algorithm is optimal if its running time is linear in the sizes of t and p, i.e., O(t+p). Perhaps one of the most interesting settings of the pattern matching problem is when one has to design an efficient algorithm with a help of a small extra space. In this paper we explore this setting to the extreme. We work under an assumption that the text t is available only in a compressed form, represented by a straight-line program. The compression methods based on efficient construction of straight-line programs are as competitive as the compression standards, including the Lempel-Ziv compression scheme and recently intensively studied text compression via block sorting, due to Burrows and Wheeler. Our main result is an algorithm that solves the compressed string matching problem in an optimal linear time, with a help of a constant extra space. We also discuss an efficient implementation of a version our algorithm showing that the new concept may have also some interesting real applications. Our result is in contrast with many other compressed pattern matching algorithms where the goal is to find all pattern occurrences in time related to the size of the compressed text. However one must remember that all previous algorithms used at least a linear (in a compressed text, a dictionary, or a pattern) extra memory while our algorithm can be implemented in a constant size extra space. Also from the practical point of view, when the compression ratio is constant (very rarely smaller than 25%), there is no dramatic difference between the running time based on the size of the compressed text and the size of the original text, while an extra space resources might be strictly limited. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

We propose a symbolic verification method for directory-based consistency protocols working for an arbitrary number of controlled resources and competing processes. We use a graph-based language to specify in a uniform way both client/server interaction schemes and manipulation of directories that contain the access rights of individual clients. Graph transformations model the dynamics of a given protocol. Universally quantified conditions defined on the labels of edges incident to a given node are used to model inspection of directories, invalidation loops and integrity conditions. Our verification procedure computes an approximated backward reachability analysis by using a symbolic representation of sets of configurations. Termination is ensured by using the theory of well-quasi orderings. [ABSTRACT FROM AUTHOR]

In [19], Yen defines a class of formulas for paths in Petri nets and claims that its satisfiability problem is EXPSPACE-complete. In this paper, we show that in fact the satisfiability problem for this class of formulas is as hard as the reachability problem for Petri nets. Moreover, we salvage almost all of Yen's results by defining a fragment of this class of formulas for which the satisfiability problem is EXPSPACE-complete by adapting his proof. [ABSTRACT FROM AUTHOR]

In this work, we consider Discrete-Time Continuous-Space Dynamic Systems for which we study the computability of the standard semantics of CTL* (CTL, LTL) and provide a variant thereof computable in the sense of Type-2 Theory of Effectivity. In particular, we show how the computable model checking of existentially and universally quantified path formulae of LTL can be reduced to solving, respectively, repeated reachability and persistence problems on a model obtained as a parallel composition of the original one and a non-deterministic Büchi automaton corresponding to the verified LTL formula. [ABSTRACT FROM AUTHOR]

In this survey, we compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. All these languages - matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models - describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, and ease of use. Moreover, they provide different support for checking the well-formedness of a model and for analyzing a model. [ABSTRACT FROM AUTHOR]

In the theory of automata over infinite alphabets, a central difficulty is that of finding a suitable compromise between expressiveness and algorithmic complexity. We propose an automaton model where we count the multiplicity of data values on an input word. This is particularly useful when such languages represent behaviour of systems with unboundedly many processes, where system states carry such counts as summaries. A typical recognizable language is: "every process does at most k actions labelled a". We show that emptiness is elementarily decidable, by reduction to the covering problem on Petri nets. [ABSTRACT FROM AUTHOR]

We show a reduction of Hilbert's tenth problem to the solvability of the matrix equation $X_1^{i_1}X_2^{i_2}\cdots X_k^{i_k} = Z$ over non-commuting integral matrices, where Z is the zero matrix, thus proving that the solvability of the equation is undecidable. This is in contrast to the case whereby the matrix semigroup is commutative in which the solvability of the same equation was shown to be decidable in general. The restricted problem where k = 2 for commutative matrices is known as the "A-B-C Problem" and we show that this problem is decidable even for a pair of non-commutative matrices over an algebraic number field. [ABSTRACT FROM AUTHOR]

The present special issue of Information and Computation journal is devoted to the 9th International Workshop on Reachability Problems (RP 2015) held on September 21-23, 2015, at the University of Warsaw. This volume contains four papers that were selected because of their overall quality and significance among 20 papers presentation at the Ninth International Workshop on Reachability Problems (RP 2015). The papers of this special issue cover foundational and pragmatic aspects of reachability problems for real-time, infinite-state and hybrid computational models. [Extracted from the article]