Search

We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper- and lower-bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: we prove (1) that the reachability problem for COCA with global upper- and lower-bound tests is in NC 2 ; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is NP-complete for COCA with parametric counter updates and bound tests.

The reachability problem on directed graphs, asking whether two vertices are connected via a directed path, is an elementary problem that has been well-studied. In this paper, we study a variation of the elementary reachability problem, called the sink-reachability problem, which can be found in many applications such as static program analysis, social network analysis, large scale web graph analysis, XML document link path analysis, and the study of gene regulation relationships. To scale sink-reachablity analysis to large graphs, we develop a highly scalable sink-reachability preserving graph reduction strategy for input sink graphs, by using a composition framework. That is, individual sink-reachability preserving condensation operators, each running in linear time, are pipelined together to produce graph reduction algorithms that result in close to maximum reduction, while keeping the computation efficient. Experiments on large real-world sink graphs demonstrate the efficiency and effectiveness of our compositional approach to sink-reachability preserving graph reduction with a reduction rate of up to 99.74% for vertices and a rate of up to 99.46% for edges.

SMPT (for Satisfiability Modulo Petri Net) is a model checker for reachability problems in Petri nets. It started as a portfolio of methods to experiment with symbolic model checking, and was designed to be easily extended. Some distinctive features are its ability to benefit from structural reductions and to generate verdict certificates. Our tool is quite mature and performed well compared to other state-of-the-art tools in the Model Checking Contest., FM 2023 - 25th International Symposium on Formal Methods,, Mar 2023, L{\"u}beck, Germany

In 2014, Jeandel proved that two dynamical properties regarding Turing machines can be computable with any desired error ϵ > 0 , the Turing machine Maximum Speed and Topological Entropy. Both problems were proved in parallel, using equivalent properties. Those results were unexpected, as most (if not all) dynamical properties are undecidable. Nevertheless, Topological Entropy positiveness for reversible and complete Turing machines was shortly proved to be undecidable, with a reduction of the halting problem with empty counters in 2-reversible Counter machines. Unfortunately, the same proof could not be used to prove undecidability of Speed Positiveness. In this research, we prove the undecidability of Homogeneous Tape Reachability Problem for aperiodic and reversible Turing machines, in order to use it to prove the undecidability of the Speed Positiveness Problem for complete and reversible Turing machines.

This work introduces a general formulation of the reconfiguration problem for untimed discrete-event systems (DES), which can be treated directly by supervisory control theory (SCT). To model the reconfiguration requirements we introduce the concept of reconfiguration specification (RS); here reconfiguration events (RE) are introduced to force a transition from one system configuration to another. Standard SCT synthesis is employed to obtain a reconfiguration supervisor (RSUP) in which designated states serve as the source states for RE. The reconfiguration problem itself is formulated as that of establishing guaranteed finite reachability of a desired RE source state in RSUP from the current state in RSUP at which a change in configuration is commanded by an external user. The solvability (or otherwise) of this reachability problem is established by backtracking as in standard dynamic programming., 2017 14th International Conference on Electrical Engineering, Computing Science and Automatic Control (CCE)

We prove that the reachability problem for two-dimensional vector addition systems with states is NL-complete or PSPACE-complete, depending on whether the numbers in the input are encoded in unary or binary. As a key underlying technical result, we show that, if a configuration is reachable, then there exists a witnessing path whose sequence of transitions is contained in a bounded language defined by a regular expression of pseudo-polynomially bounded length. This, in turn, enables us to prove that the lengths of minimal reachability witnesses are pseudo-polynomially bounded.

This paper addresses the problem of verifying discrete-time stochastic systems against omega-regular specifications using finite-state abstractions. Omega-regular properties allow specifying complex behavior and encompass, for example, linear temporal logic. We focus on a class of systems with mixed monotone dynamics. This class has recently been show to be amenable to efficient reachable set computation and models a wide-range of physically relevant systems. In general, finite-state abstractions of continuous state stochastic systems give rise to augmented Markov Chains wherein the probabilities of transition between states are restricted to an interval. We present a procedure to compute a finite-state Interval-valued Markov Chain abstraction of discrete-time, mixed monotone stochastic systems subject to affine disturbances given a rectangular partition of the state-space. Then, we suggest an algorithm for performing verification against omega-regular properties in IMCs. Specifically, we aim to compute bounds on the probability of satisfying the specification of interest from any initial state in the IMC. This is achieved by solving a reachability problem on sets of so-called winning and losing components in the Cartesian product between the IMC and a Rabin automaton representing the specification. Next, the verification of IMCs may yield a set of states whose acceptance status is undecided with respect to the specification, requiring a refinement of the abstraction. We describe a specification-guided approach that compares the best-case and worst-case behaviors of accepting paths in the IMC and targets the appropriate states accordingly. Finally, we show a case study.

We study the reachability problem for queue automata and lossy queue automata. Concretely, we consider the set of queue contents which are forwards resp. backwards reachable from a given set of queue contents. Here, we prove the preservation of regularity if the queue automaton loops through some special sets of transformation sequences. This is a generalization of the results by Boigelot et al. and Abdulla et al. regarding queue automata looping through a single sequence of transformations. We also prove that our construction is possible in polynomial time.

Randomized higher-order computation can be seen as being captured by a λ-calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice. What matters about such computations is the probability of obtaining any given result, rather than the possibility or the necessity of obtaining it, like in (non)deterministic computation. Termination, arguably the simplest kind of reachability problem, can be spelled out in at least two ways, depending on whether it talks about the probability of convergence or about the expected evaluation time, the second one providing a stronger guarantee. In this paper, we show that intersection types are capable of precisely characterizing both notions of termination inside a single system of types: the probability of convergence of any λ-term can be underapproximated by its type , while the underlying derivation’s weight gives a lower bound to the term’s expected number of steps to normal form. Noticeably, both approximations are tight—not only soundness but also completeness holds. The crucial ingredient is non-idempotency, without which it would be impossible to reason on the expected number of reduction steps which are necessary to completely evaluate any term. Besides, the kind of approximation we obtain is proved to be optimal recursion theoretically: no recursively enumerable formal system can do better than that.

We study the problem of verifying the robustness of concurrent programs against a C11-style memory model that includes relaxed accesses and release/acquire accesses and fences, and show that this verification problem can be reduced to a standard reachability problem under sequential consistency. We further observe that existing robustness notions do not allow the verification of programs that use speculative reads as in the sequence lock mechanism, and introduce a novel "observational robustness" property that fills this gap. In turn, we show how to soundly check for observational robustness. We have implemented our method and applied it to several challenging concurrent algorithms, demonstrating the applicability of our approach. To the best of our knowledge, this is the first method for verifying robustness against a programming language concurrency model that includes relaxed accesses and release/acquire fences.

Reachability analysis of nonlinear dynamical systems is a challenging and computationally expensive task. Computing the reachable states for linear systems, in contrast, can often be done efficiently in high dimensions. In this paper, we explore verification methods that leverage a connection between these two classes of systems based on the concept of the Koopman operator. The Koopman operator links the behaviors of a nonlinear system to a linear system embedded in a higher dimensional space, with an additional set of so-called observable variables. Although, the new dynamical system has linear differential equations, the set of initial states is defined with nonlinear constraints. For this reason, existing approaches for linear systems reachability cannot be used directly. In this paper, we propose the first reachability algorithm that deals with this unexplored type of reachability problem. Our evaluation examines several optimizations, and shows the proposed workflow is a promising avenue for verifying behaviors of nonlinear systems., Comment: Extended version of the paper accepted at ADHS 2021

Reachability analysis is one of the most basic and challenging problems in verification. We investigate this problem in multi-agent reinforcement learning (MARL) system by transforming the reachability analysis to decision-making problem tackled by mixed integer linear programming (MILP) solver Gurobi. We define syntax and semantics for multi-role strategy logic (mrSL) which is used to describe the reachability specification. The logic mrSL is a variant of SL to express properties, which provide a holistic perspective to describe reachability properties instead of specifying a specific agent reaches a certain state in the MARL system. And the algorithms to translate reachability property into MILP constraints are provided. A tool called MAReachAnalysis is introduced, which uses Gurobi to solve the corresponding reachability problem and evaluate it on the predator-prey task of multi-agent deep deterministic policy gradient (MADDPG) example, discussion of the experimental results obtained on a range of test cases.

Algorithms and protocols with time dependent behavior are often specified formally using timed automata. For practical real-time systems, besides real-valued clock variables, these specifications typically contain discrete data variables with nontrivial data flow. In this paper, we propose a configurable lazy abstraction framework for the location reachability problem of timed automata that potentially contain discrete variables. Moreover, based on our previous work, we uniformly formalize in our framework several abstraction refinement strategies for both clock and discrete variables that can be freely combined, resulting in many distinct algorithm configurations. Besides the proposed refinement strategies, the configurability of the framework allows the integration of existing efficient lazy abstraction algorithms for clock variables based on $${\textit{LU}}$$ LU -bounds. We demonstrate the applicability of the framework and the proposed refinement strategies by an empirical evaluation on a wide range of timed automata models, including ones that contain discrete variables or diagonal constraints.

© 2020, Springer-Verlag GmbH Germany, part of Springer Nature. Constrained reachability is a kind of quantitative path property, which is generally specified by multiphase until formulas originated in continuous stochastic logic. In this paper, through proposing a positive operator valued measure on the set of infinite paths, we develop an exact method to solve the constrained reachability problem for quantum Markov chains. The convergence rate of the reachability is also obtained. We then analyse the complexity of the proposed method, which turns out to be in polynomial-time w.r.t. the size of the classical state space and the dimension of the accompanied Hilbert space. Finally, our method is implemented and applied to a simple quantum protocol.

The problem of reachability on graphs with restriction is studied. Such restrictions mean that only those paths that satisfy certain conditions are valid paths on the graph. Because of this, for classical optimization problems one has to consider only a subset of feasible paths on the graph, which significantly complicates their solution. Reachability constraints arise naturally in various applied problems, for example, in the problem of navigation in telecommunication networks with areas of strong signal attenuation or when modeling technological processes in which there is a condition for the order of actions or the compatibility of operations. General concepts of a graph with non-standard reachability and a valid path on it are introduced. It is shown that the classical graphs, as well as graphs with restrictions on passing through the selected arcs subsets are special cases of graphs with non-standard reachability. General approach to solving the shortest path problem on a graph with non-standard achievability is developed. This approach consists in constructing an auxiliary graph and reducing the shortest path problem on a graph with non-standard reachability to a similar problem on an auxiliary graph. The theorem on the correspondence of the paths of the original and auxiliary graphs is proved.

This study investigates the set reachability of Markovian jump Boolean networks (MJBNs). Firstly, through comprehensive analysis, two kinds of set reachability, strong set reachability and weak set reachability, are defined. By using semi-tensor product of matrices, the considered MJBN is converted into a Markov chain which can not only describe the state transition of the MJBN synchronously, but also maintain its transition probability. Based on this, the set reachability problem of the MJBN is transformed into the reachability and convergence problems of the corresponding Markov chain. Then some necessary and sufficient conditions for set reachability of MJBNs are obtained. Finally, the observability and output stability problems of MJBNs are discussed as two applications of set reachability.

In this paper, we propose a new approach to solving the backward reachability problem for nonlinear dynamical systems. Previously, this class of problems has been studied within frameworks of optimal control and zero-sum differential games, where a backward reachable set can be expressed as the zero sublevel set of the value function that can be characterized by solving the Hamilton-Jacobi-Bellman (HJB) partial differential equation (PDE). In many cases, however, a high computational cost is incurred in numerically solving such HJB PDEs due to the curse of dimensionality. We use the pseudospectral method to convert the associated optimal control problem into nonlinear programs (NLPs). We then show that the zero sublevel set obtained by the optimal cost of the NLP is the corresponding backward reachable set. Note that our approach does not require solving complex HJB PDEs. Therefore, it can reduce computation time and handle high-dimensional dynamical systems, compared with the numerical software package developed by I. Mitchell, which has been used widely in the literature to obtain backward reachable sets by solving HJB equations. We provide several examples to validate the effectiveness of the proposed approach.

This paper presents a decentralised periodic interpolating control (dpIC) scheme for the constrained control of interconnected systems, which employs periodic invariance and vertex reachability of target sets. Periodic invariance allows the state of the system to leave a candidate set temporarily but return into the set in a finite number of steps. We consider a periodic invariant set with low-complexity (e.g. rectangle, hexagon for planar systems) to replace the expensive controllable invariant outer set. This set is defined within the controllable stabilising region of each subsystem and a reachability problem is solved off-line for each vertex of the outer set to provide an admissible control sequence that steers the system state back into the original target set after a finite number of steps. dpIC is effectuated between such periodic invariant sets for each subsystem and the local maximal admissible inner set by means of an inexpensive linear programming problem, which is solved on-line at the beginning of each periodic control sequence. dpIC is demonstrated on the problem of stabilising a platoon of vehicles.

A rotor walk in a directed graph can be thought of as a deterministic version of a Markov Chain, where a pebble moves from vertex to vertex following a simple rule until a terminal vertex, or sink, has been reached. The ARRIVAL problem, as defined by Dohrau et al. [Dohrau et al., 2017], consists in determining which sink will be reached. While the walk itself can take an exponential number of steps, this problem belongs to the complexity class NP ∩ co-NP without being known to be in P. In this work, we define a class of directed graphs, namely tree-like multigraphs, which are multigraphs having the global shape of an undirected tree. We prove that in this class, ARRIVAL can be solved in almost linear time, while the number of steps of a rotor walk can still be exponential. Then, we give an application of this result to solve some deterministic analogs of stochastic models (e.g., Markovian decision processes, Stochastic Games)., LIPIcs, Vol. 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), pages 12:1-12:14

Petri nets, equivalently presentable as vector addition systems with states, are an established model of concurrency with widespread applications. The reachability problem, where we ask whether from a given initial configuration there exists a sequence of valid execution steps reaching a given final configuration, is the central algorithmic problem for this model. The complexity of the problem has remained, until recently, one of the hardest open questions in verification of concurrent systems. A first upper bound has been provided only in 2015 by Leroux and Schmitz, then refined by the same authors to non-primitive recursive Ackermannian upper bound in 2019. The exponential space lower bound, shown by Lipton already in 1976, remained the only known for over 40 years until a breakthrough non-elementary lower bound by Czerwi��ski, Lasota, Lazic, Leroux and Mazowiecki in 2019. Finally, a matching Ackermannian lower bound announced this year by Czerwi��ski and Orlikowski, and independently by Leroux, established the complexity of the problem. Our primary contribution is an improvement of the former construction, making it conceptually simpler and more direct. On the way we improve the lower bound for vector addition systems with states in fixed dimension (or, equivalently, Petri nets with fixed number of places): while Czerwi��ski and Orlikowski prove F_k-hardness (hardness for kth level in Grzegorczyk Hierarchy) in dimension 6k, our simplified construction yields F_k-hardness already in dimension 3k+2., LIPIcs, Vol. 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022), pages 46:1-46:15

We briefly describe recent advances on understanding the complexity of the reachability problem for vector addition systems (or equivalently for vector addition systems with states - VASSes). We present a zoo of a few involved VASS examples, which illustrate various aspects of hardness of VASSes and various techniques of proving lower complexity bounds., LIPIcs, Vol. 243, 33rd International Conference on Concurrency Theory (CONCUR 2022), pages 5:1-5:13

We study the reachability problem for affine $\mathbb{Z}$-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine $\mathbb{Z}$-VASS with the finite-monoid property (afmp-$\mathbb{Z}$-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-$\mathbb{Z}$-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-$\mathbb{Z}$-VASS reduces to reachability in a $\mathbb{Z}$-VASS whose control-states grow linearly in the size of the matrix monoid. Our construction shows that reachability relations of afmp-$\mathbb{Z}$-VASS are semilinear, and in particular enables us to show that reachability in $\mathbb{Z}$-VASS with transfers and $\mathbb{Z}$-VASS with copies is PSPACE-complete. We then focus on the reachability problem for affine $\mathbb{Z}$-VASS with monogenic monoids: (possibly infinite) matrix monoids generated by a single matrix. We show that, in a particular case, the reachability problem is decidable for this class, disproving a conjecture about affine $\mathbb{Z}$-VASS with infinite matrix monoids we raised in a preliminary version of this paper. We complement this result by presenting an affine $\mathbb{Z}$-VASS with monogenic matrix monoid and undecidable reachability relation.

Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations with respect to arbitrary classes of affine operations. More specifically, we provide a trichotomy on the complexity of integer reachability in VASS extended with affine operations (affine VASS). Namely, we show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with (pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other class. We further present a dichotomy for standard reachability in affine VASS: it is decidable for VASS with permutations, and undecidable for any other class. This yields a complete and unified complexity landscape of reachability in affine VASS. We also consider the reachability problem parameterized by a fixed affine VASS, rather than a class, and we show that the complexity landscape is arbitrary in this setting.

We consider parameterized verification of concurrent programs under the Total Store Order (TSO) semantics. A program consists of a set of processes that share a set of variables on which they can perform read and write operations. We show that the reachability problem for a system consisting of an arbitrary number of identical processes is PSPACE-complete. We prove that the complexity is reduced to polynomial time if the processes are not allowed to read the initial values of the variables in the memory. When the processes are allowed to perform atomic read-modify-write operations, the reachability problem has a non-primitive recursive complexity.

Fix an algebraic structure ( A , ⁎ ) . Given a graph G = ( V , E ) and the labelling function ϕ ( ϕ : E → A ) for the edges, two nodes s , t ∈ V , and a subset F ⊆ A , the A - Reach problem asks if there is a path p (need not be simple) from s to t whose yield (result of the operation in the ordered set of the labels of the edges constituting the path) is in F . On the complexity frontier of this problem, we show the following results. • When A is a group whose size is polynomially bounded in the size of the graph (hence equivalently presented as a multiplication table at the input), and the graph is undirected, the A - Reach problem is in L . Building on this, using a decomposition in [4] , we show that, when A is a fixed quasi-group, and the graph is undirected, the A - Reach problem is in L . In a contrast, we show NL -hardness of the problem over bidirected graphs, when A is a matrix group over Q , or an aperiodic monoid. • As our main theorem, we prove a dichotomy for graphs labelled with fixed aperiodic monoids by showing that for every fixed aperiodic monoid A , A - Reach problem is either in L or is NL -complete. • We show that there exists a monoid M , such that the reachability problem in general DAGs can be reduced to A - Reach problem for planar non-bipartite DAGs labelled with M . In contrast, we show that if the planar DAGs that we obtain above are bipartite, the problem can be further reduced to reachability testing in planar DAGs and hence is in UL .

We show second-order decidability results on recognizable tree languages and one-pass reduction sequences with special term rewriting systems. For some classes of term rewriting systems the second-order IO one-pass inclusion problem, the second-order IO one-pass reachability problem, and the IO and OI one-pass common ancestor problems are decidable.

A communicating system is \(k\)-synchronizable if all of the message sequence charts representing the executions can be divided into slices of k sends followed by k receptions. It was previously shown that, for a fixed given k, one could decide whether a communicating system is \(k\)-synchronizable. This result is interesting because the reachability problem can be solved for \(k\)-synchronizable systems. However, the decision procedure assumes that the bound k is fixed. In this paper we improve this result and show that it is possible to decide if such a bound k exists.

Stealthy attacks on Industrial Control Systems can cause significant damage while evading detection. In this paper, instead of focusing on the detection of stealthy attacks, we aim to provide early warnings to operators, in order to avoid physical damage and preserve in advance data that may serve as an evidence during an investigation. We propose a framework to provide grounds for suspicion, i.e. preliminary indicators reflecting the likelihood of success of a stealthy attack. We propose two grounds for suspicion based on the behaviour of the physical process: (i) feasibility of a stealthy attack, and (ii) proximity to unsafe operating regions. We propose a metric to measure grounds for suspicion in real-time and provide soundness principles to ensure that such a metric is consistent with the grounds for suspicion. We apply our framework to Linear Time-Invariant (LTI) systems and formulate the suspicion metric computation as a real-time reachability problem. We validate our framework on a case study involving the benchmark Tennessee-Eastman process. We show through numerical simulation that we can provide early warnings well before a potential stealthy attack can cause damage, while incurring minimal load on the network. Finally, we apply our framework on a use case to illustrate its usefulness in supporting early evidence collection.

We give an almost quadratic n2−o(1) lower bound on the space consumption of any o(√logn)-pass streaming algorithm solving the (directed) s-t reachability problem. This means that any such algorithm must essentially store the entire graph. As corollaries, we obtain almost quadratic space lower bounds for additional fundamental problems, including maximum matching, shortest path, matrix rank, and linear programming. Our main technical contribution is the definition and construction of set hiding graphs, that may be of independent interest: we give a general way of encoding a set S ⊆ [k] as a directed graph with n = k 1 + o( 1 ) vertices, such that deciding whether i ∈ S boils down to deciding if ti is reachable from si, for a specific pair of vertices (si,ti) in the graph. Furthermore, we prove that our graph “hides” S, in the sense that no low-space streaming algorithm with a small number of passes can learn (almost) anything about S.

International audience; Vector addition systems with states (VASS for short), or equivalently Petri nets are one of the most popular formal methods for the representation and the analysis of parallel processes. The central algorithmic problem is reachability: whether from a given initial configuration there exists a sequence of valid execution steps that reaches a given final configuration. This paper provides an overview of results about the reachability problem for VASS related to Presburger arithmetic, by presenting 1) a simple algorithm for deciding the reachability problem based on invariants definable in Presburger arithmetic, 2) the class of flat VASS for computing reachability sets in Presburger arithmetic, and 3) complexity results about the reachability problem for flat VASS.

Petri nets are an important formal paradigm for modeling and analysis of discrete event systems. The related areas of application of Petri nets include deadlock avoidance and prevention, supervisory control, forbidden state detection, different aspects of flexible manufacturing systems, and many others (Zhou & DiCesare, 1993; Holloway et al., 1997; Boel et al., 1995). Quite often, given a discrete-event system, the designer is interested in determining whether the system can transit from an initial state to another, target state as a result of some operations from a predefined set. In terms of Petri nets, the answer to this question is obtained as a solution of a reachability problem. The reachability problem in Petri nets is formulated as follows: for any Petri net PN, with an initial marking M0, and for some other marking M, determine whether the relation M ∈ R(PN, M0) is true, where R(PN, M0) is the reachability set of PN for its initial marking M0 (Murata, 1989). The decidability of the reachability problem has been proved for a number of restricted classes of Petri nets, and there are efficient algorithms for such classes as acyclic Petri nets, marked graphs, and others (Kodama & Murata, 1988; Caprotti et al., 1995; Kostin, 1997). It has been shown that the reachability problem is decidable for generalized Petri nets as well (Mayr, 1984). The fundamental contribution of the paper (Mayr, 1984) is in proving that the reachability problem for generalized Petri nets is decidable. However, being highly important theoretically, the practical use of the algorithm described in that paper is limited. Actually, the algorithm creates a series of so called regular constrained refined graphs, each of which is a generalization of the basic coverability tree. As the author admits, the first refined graph would enumerate the whole reachability set of the given Petri net. In practice, two different approaches are used most often to determine the reachability of a marking in Petri nets. The first approach is based on the creation and investigation of a complete or reduced reachability graph. The main drawback of this approach is a state explosion problem. A closely related technique is the use of stubborn sets. The main purpose of the stubborn sets technique is to choose, for each marking of the net, a set of transitions to fire that is large enough to preserve some desired information about the Petri net, but is as small as possible to get a significant reduction of the resulting reachability graph (Varpaaniemi, 1998). Unfortunately, generation of minimal or reduced reachability graphs in finite state systems is known to be an NP-hard problem (Peled, 1993). If Petri net has no

Concurrent accesses to databases are typically encapsulated in transactions in order to enable isolation from other concurrent computations and resilience to failures. Modern databases provide transactions with various semantics corresponding to different trade-offs between consistency and availability. Since a weaker consistency model provides better performance, an important issue is investigating the weakest level of consistency needed by a given program (to satisfy its specification). As a way of dealing with this issue, we investigate the problem of checking whether a given program has the same set of behaviors when replacing a consistency model with a weaker one. This property known as robustness generally implies that any specification of the program is preserved when weakening the consistency. We focus on the robustness problem for consistency models which are weaker than standard serializability, namely, causal consistency, prefix consistency, and snapshot isolation. We show that checking robustness between these models is polynomial time reducible to a state reachability problem under serializability. We use this reduction to also derive a pragmatic proof technique based on Lipton's reduction theory that allows to prove programs robust. We have applied our techniques to several challenging applications drawn from the literature of distributed systems and databases., 38 pages, 7 figures, 2 tables, extended version of ESOP 2021 conference paper

Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as A* and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis., Comment: 29 pages, 13 figures

We consider the reachability problem for finite-state multi-threaded programs under the promising semantics () of Lee et al., which captures most common program transformations. Since reachability is already known to be undecidable in the fragment of with only release-acquire accesses (-), we consider the fragment with only relaxed accesses and promises (). We show that reachability under is undecidable in general and that it becomes decidable, albeit non-primitive recursive, if we bound the number of promises.Given these results, we consider a bounded version of the reachability problem. To this end, we bound both the number of promises and of “view-switches”, i.e., the number of times the processes may switch their local views of the global memory. We provide a code-to-code translation from an input program under (with relaxed and release-acquire memory accesses along with promises) to a program under SC, thereby reducing the bounded reachability problem under to the bounded context-switching problem under SC. We have implemented a tool and tested it on a set of benchmarks, demonstrating that typical bugs in programs can be found with a small bound.