Search

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.

Object sensitivity is widely used as a context abstraction for computing the points-to information context-sensitively for object-oriented programming languages such as Java. Due to the combinatorial explosion of contexts in large object-oriented programs, k -object-sensitive pointer analysis (under k -limiting), denoted k -obj , is often inefficient even when it is scalable for small values of k , where k ⩽ 2 holds typically. A recent popular approach for accelerating k -obj trades precision for efficiency by instructing k -obj to analyze only some methods in a program context-sensitively, determined heuristically by a pre-analysis. In this article, we investigate how to develop a fundamentally different approach, Eagle , for designing a pre-analysis that can make k -obj run significantly faster while maintaining its precision. The novelty of Eagle is to enable k -obj to analyze a method with partial context sensitivity (i.e., context-sensitively for only some of its selected variables/allocation sites) by solving a context-free-language (CFL) reachability problem based on a new CFL-reachability formulation of k -obj . By regularizing one CFL for specifying field accesses and using another CFL for specifying method calls, we have formulated Eagle as a fully context-sensitive taint analysis (without k -limiting) that is both effective (by selecting the variables/allocation sites to be analyzed by k -obj context-insensitively so as to reduce the number of context-sensitive facts inferred by k -obj in the program) and efficient (by running linearly in terms of the number of pointer assignment edges in the program). As Eagle represents the first precision-preserving pre-analysis, our evaluation focuses on demonstrating its significant performance benefits in accelerating k -obj for a set of popular Java benchmarks and applications, with call graph construction, may-fail-casting, and polymorphic call detection as three important client analyses.

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.

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.

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.

Conditional pushdown systems (CPDSs) extend pushdown systems by associating each transition rule with a regular language over the stack alphabet. The goal is to model program verification problems that need to examine the runtime call stack of programs. Examples include security property checking of programs with stack inspection, compatibility checking of HTML5 parser specifications, etc. Esparza et al. proved that the reachability problem of CPDSs is EXPTIME-complete, which prevents the existence of an algorithm tractable for all instances in general. Driven by the practical applications of CPDSs, we study the reachability of patterned CPDS (pCPDS) that is a practically important subclass of CPDS, in which each transition rule carries a regular expression obeying certain patterns. First, we present new saturation algorithms for solving state and configuration reachability of pCPDSs. The algorithms exhibit the exponential-time complexity in the size of atomic patterns in the worst case. Next, we show that the reachability of pCPDSs carrying simple patterns is solvable in fixed-parameter polynomial time and space. This answers the question on whether there exist tractable reachability analysis algorithms of CPDSs tailored for those practical instances that admit efficient solutions such as stack inspection without exception handling. We have evaluated the proposed approach, and our experiments show that the pattern-driven algorithm steadily scales on pCPDSs with simple patterns.

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.

International audience; Polynomial Interrupt Timed Automata (PolITA) are finite automata with clocks organized along hierarchical levels. These clocks are equipped with an interruption mechanism, well suited to the modeling of real-time operating systems. Moreover, transitions between states contain polynomial guards and updates. The reachability problem in this class is known to be in 2EXPTIME with a decision procedure based on the cylindrical algebraic decomposition. We improve this complexity to EXPSPACE mainly using a combinatorial argument and we include a reduction leading to a PSPACE lower bound.

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 .

In this paper, the set reachability and observability of probabilistic Boolean networks (PBNs) are investigated. Using a parallel extension technique, we proved that the observability problem of a PBN can be recast as a set reachability problem of an interconnected PBN. For set reachability analysis, we designed a random logic dynamical system (RLDS) from the PBN under consideration by reconstructing the state transfer graph (STG). We proved that, for a PBN, a target subset is reachable from an initial subset if and only if all solutions to the corresponding RLDS starting from the initial subset converge to the zero state. Based on the STG reconstruction technique and using the largest invariant subset algorithm, the necessary and sufficient conditions for finite-time set reachability with probability one and asymptotical set reachability in distribution were obtained. All the results are expressed in terms of the transition probability matrix between non-zero states of the RLDS. Further, the results related to set reachability were applied to the observability problem of PBNs. The necessary and sufficient conditions for finite-time observability with probability one and asymptotical observability in distribution were obtained. Finally, examples were presented to illustrate the effectiveness of the proposed method.

The computational study on finite/infinite-state systems, probabilistic systems, and finite-state fuzzy systems, has received much attention recently. In contrast, there are very few results for algorithmic analysis of infinite-state fuzzy systems. In this paper, we introduce fuzzy pushdown termination games (FPDTGs), which are an extension of fuzzy pushdown automata with a game feature and can serve as a formal model of infinite-state fuzzy systems. We investigate some computational issues of the games under termination objectives for two players: the goal of player-1 is to maximize the truth value of eventually terminating at some given configurations with the empty stack, while player-2 aims at the opposite. Some interesting results are obtained. For example, we show that both players have optimal memoryless strategies and the same value. The problem of computing the value can be solved in exponential time when the triangular norm is chosen as the minimum one. Furthermore, we present efficient algorithms for computing the values of two special subclasses of FPDTGs. The potential for practical use of our model is demonstrated by a case study on a manufacturing system.

Hybrid automata are an elegant formal model seamlessly integrating differential equations representing continuous dynamics with automata capturing switching behavior. Since the introduction of the computational model more than a quarter of a century ago [Maler et al. 1992], its algorithmic verification has been an area of intense research. Within this note, which is dedicated to Oded Maler (1957--2018) as one of the inventors of the model, we are trying to delineate major lines of attack to the reachability problem for hybrid automata. Due to its relation to system safety, the reachability problem is a prototypical verification problem for hybrid discrete-continuous system dynamics.

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.

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.

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.

In rendez-vous protocols an arbitrarily large number of indistinguishable finite-state agents interact in pairs. The cut-off problem asks if there exists a number B such that all initial configurations of the protocol with at least B agents in a given initial state can reach a final configuration with all agents in a given final state. In a recent paper [17], Horn and Sangnier prove that the cut-off problem is equivalent to the Petri net reachability problem for protocols with a leader, and in "Image missing" for leaderless protocols. Further, for the special class of symmetric protocols they reduce these bounds to "Image missing" and "Image missing" , respectively. The problem of lowering these upper bounds or finding matching lower bounds is left open. We show that the cut-off problem is "Image missing" -complete for leaderless protocols, "Image missing" -complete for symmetric protocols with a leader, and in "Image missing" for leaderless symmetric protocols, thereby solving all the problems left open in [17].

We address the problem of verifying the reachability problem in programs running under the formal model Px86 defined recently by Raad et al. in POPL'20 for the persistent Intel x86 architecture. We prove that this problem is decidable. To achieve that, we provide a new formal model that is equivalent to Px86 and that has the feature of being a well structured system. Deriving this new model is the result of a deep investigation of the properties of Px86 and the interplay of its components.

Population protocols are a well established model of computation by anonymous, identical finite state agents. A protocol is well-specified if from every initial configuration, all fair executions reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is EXPSPACE-hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class WS3 of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that WS3 has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership problem for WS3 reduces to solving boolean combinations of linear constraints over N. This allowed us to develop the first software able to automatically prove well-specification for all of the infinitely many possible inputs., 29 pages, 1 figure

Virtual network function (vnf) can be useful for efficient use of cloud resources, specially for 5G networks, where dynamic creation, modification and deletion of virtual network functions are of special need. OpenStack is an open source cloud computing platform, where it is possible to create any virtual network function on demand. During creation of virtual network function, using Tacker or Mistral interface of OpenStack, the problem can arrive with respect to the reachability of vnf, which triggers the OpenStack to recreate the vnf. In this present work, we derive a closed form expression to analyze the availability of vnf considering the reachability problem during or after creation of virtual network function. Further, we compare availability of vnf considering two vnf creation procedures.

Code reuse attacks have been the subject of a substantial amount of research during the past decade. This research largely resulted from early work on Return-Oriented Programming (ROP), which showed that the then newly proposed Non-Executable Memory (NX) defense could be bypassed. More recently, the research community has been simultaneously investigating new defenses that are believed to thwart code reuse attacks, such as Control Flow Integrity (CFI), and defense-aware techniques for attacking these defenses, such as Data-Oriented Programming (DOP). Unfortunately, the feasibility of defense-aware attacks are very dependent on the behaviors of the attacked program, which makes it difficult for defenders to understand how much protection a defense such as CFI may provide. To better understand this, researchers have introduced automated defense-aware code reuse attack systems. Unfortunately, the handful of existing systems implement a single fixed, defense-specific strategy that is complex and cannot be used to consider other defenses. In this paper, we propose a generic framework for automatically discovering defense-aware code reuse attacks in executables. Unlike existing work, which utilizes hard-coded strategies for specific defenses, our framework can produce attacks for multiple defenses by analyzing the runtime behavior of the defense. The high-level insight behind our framework is that code reuse attacks can be defined as a state reachability problem, and that defenses prevent some transitions between states. We implement our framework as a tool named Limbo, which employs an existing binary concolic executor to solve the reachability problem. We evaluate Limbo and show that it excels when there is little code available for reuse, making it complementary to existing techniques. We show that, in such scenarios, Limbo outperforms existing systems that automate ROP attacks, as well as systems that automate DOP attacks in the presence of fine-grained CFI, despite having no special knowledge about ROP or DOP attacks.

Logical Methods in Computer Science ; Volume 16, Issue 4 ; 1860-5974, In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. In this paper, we initiate a study on the probabilistic higher-order model checking problem, by giving some first theoretical and experimental results. As a first step towards our goal, we introduce PHORS, a probabilistic extension of higher-order recursion schemes (HORS), as a model of probabilistic higher-order programs. The model of PHORS may alternatively be viewed as a higher-order extension of recursive Markov chains. We then investigate the probabilistic termination problem -- or, equivalently, the probabilistic reachability problem. We prove that almost sure termination of order-2 PHORS is undecidable. We also provide a fixpoint characterization of the termination probability of PHORS, and develop a sound (but possibly incomplete) procedure for approximately computing the termination probability. We have implemented the procedure for order-2 PHORSs, and confirmed that the procedure works well through preliminary experiments that are reported at the end of the article.

Part 1: Full Papers; International audience; Clock-dependent probabilistic timed automata extend classical timed automata with discrete probabilistic choice, where the probabilities are allowed to depend on the exact values of the clocks. Previous work has shown that the quantitative reachability problem for clock-dependent probabilistic timed automata with at least three clocks is undecidable. In this paper, we consider the subclass of clock-dependent probabilistic timed automata that have one clock, that have clock dependencies described by affine functions, and that satisfy an initialisation condition requiring that, at some point between taking edges with non-trivial clock dependencies, the clock must have an integer value. We present an approach for solving in polynomial time quantitative and qualitative reachability problems of such one-clock initialised clock-dependent probabilistic timed automata. Our results are obtained by a transformation to interval Markov decision processes.

International audience; Deciding privacy-type properties of deterministic cryptographic protocols such as anonymity and strong secrecy can be reduced to deciding the symbolic equivalence of processes, where each process is described by a set of possible symbolic traces. This equivalence is parameterized by a deduction system that describes which actions and observations an intruder can perform on a running system. We present in this paper a notion of finitary deduction systems. For this class of deduction system, we first reduce the problem of the equivalence of processes with no disequations to the resolution of reachability problem on each symbolic trace of one process, and then testing whether each solution found is solution of a related trace in the other process. We then extend this reduction to the case of generic deterministic finite processes in which symbolic traces may contain disequalities.

It is ``folklore'' that the solution to a set reachability problem for a dynamical system is only noncomputable because of non-robustness reasons. A robustness condition that can be imposed on a dynamical system is the requirement of the chain reachable set to equal the closure of the reachable set. We claim that this condition necessarily imposes strong conditions on the dynamical system. For instance, if the space is connected and compact and we are computing a chain reachable robust single valued function $f$ then $f$ cannot have an unstable fixed point or unstable periodic cycle., 15 pages, 0 figures. Extended conference proceedings submitted to IFAC 2020

The reachability problem for timed automata asks if a given automaton has a run leading to an accepting state, and the liveness problem asks if the automaton has an infinite run that visits accepting states infinitely often. Both of these problems are known to be P space -complete. We show that if P ≠P space , the liveness problem is more difficult than the reachability problem; in other words, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is P space -hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it to existing solutions.

In a previous paper we introduced immediate observation Petri nets [9], a subclass of Petri nets with application domains in distributed protocols and theoretical chemistry (chemical reaction networks). IO nets enjoy many useful properties [9, 14], but like the general case of conservative Petri nets they have a PSPACE-complete reachability problem. In this paper we explore two restrictions of the reachability problem for IO nets which lower the complexity of the problem drastically. The complexity is NP-complete for the first restriction with applications in distributed protocols, and it is polynomial for the second restriction with applications in chemical settings.

Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in analyzing a restricted class which still captures useful behaviors. In this paper, we propose a new class of bounded underapproximations for multi-pushdown systems, which subsumes most existing classes. We develop an efficient algorithm for solving the under-approximate reachability problem, which is based on efficient fix-point computations. We implement it in our tool BHIM and illustrate its applicability by generating a set of relevant benchmarks and examining its performance. As an additional takeaway BHIM solves the binary reachability problem in pushdown automata. To show the versatility of our approach, we then extend our algorithm to the timed setting and provide the first implementation that can handle timed multi-pushdown automata with closed guards.

International audience; We consider the decidability of state-to-state reachability in linear time-invariant control systems over continuous time. We analyze this problem with respect to the allowable control sets, which are assumed to be the image under a linear map of the unit hypercube (i.e. zonotopes). This naturally models bounded (sometimes called saturated) controls. Decidability of the version of the reachability problem in which control sets are affine subspaces of R is a fundamental result in control theory. Our first result is decidability in two dimensions (= 2) if matrix satisfies some spectral conditions and conditional decidablility in general. If the transformation matrix is diagonal with rational entries (or rational multiples of the same algebraic number) then the reachability problem is decidable. If the transformation matrix only has real eigenvalues, the reachability problem is conditionally decidable. The time-bounded reachability problem is conditionally decidable and unconditionally decidable in two dimensions. Some of our results rely on the decidability of certain logical theories-namely the theory of the reals with exponential (ℜ exp) and with bounded sine (ℜ exp,sin)-which have been proven decidable conditional on Schanuel's Conjecture-a unifying conjecture in transcendence theory. We also obtain a hardness result for a mild generalization of the problem where the target is a simple set (hypercube of dimension − 1 or hyperplane) instead of a point. In this case, we show that the problem is at least as hard as the Continuous Positivity problem if the control set is a singleton, or the Nontangential Continuous Positivity problem if the control set is [−1, 1]. CCS CONCEPTS • Computing methodologies → Computational control theory.

Hybrid Systems are systems having a mixed discrete and continuous behaviour that cannot be characterized faithfully using either only discrete or only continuous models. A good framework for hybrid systems should support their compositional description and analysis, since commonly systems are specified by a composition of smaller subsystems, to cope with the complexity of their monolithic representation. Moreover, since the reachability problem for hybrid systems is undecidable, one should investigate the conditions that guarantee approximate computability of composition, when only approximations to the exact problem data are available.In this paper, we propose an automata-based formalism (HIOA) for hybrid systems that is compositional and for which the evolution can be computed approximately. The main results are that the composition of compatible HIOA yields a pre-HIOA; a dominance result on the composition of HIOA by which we can replace any component in a composition by another one that exhibits the same external behaviour without affecting the behaviour of the composition; finally, the key result that the composition of two compatible upper(lower)-semicontinuous HIOA is a computable upper(lower)-semicontinuous pre-HIOA, which entails that the evolution of the composition is upper(lower)-semicomputable. A discussion on how compositionality/computability are handled in state-of-art libraries for reachability analysis closes the paper.

International audience; We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendezvous between parallel threads with communicating pushdown systems (from now on CPDSs). The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed. To this end, an algebraic framework to over-approximate context-free languages has been introduced by Bouajjani et al. In this paper, we combine this framework with an automata-theoretic approach in order to approximate an answer to the model checking problem of the lineartime temporal logic (from now on LTL) on CPDSs. We then present an algorithm that, given a single-indexed or stutter-invariant LTL formula, allows us to prove that no run of a CPDS verifies this formula if the procedure ends.

International audience; This work tackles the reachability problem of uncertain discrete-time linear systems controlled by estimated state feedback regulators. First an augmented system is considered in order to include the effect of the estimation error on the behavior of the closed loop system. Then, based on interval analysis, an interval predictor is proposed to compute tight trajectory tubes that contain in a guaranteed way the actual state trajectory of the augmented system. Moreover, under the standard controllability and observability assumptions of linear systems, the convergence of the width of these trajectory tubes is shown.

We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads. Our main result shows that context-bounded fair termination is decidable for the model; context-bounded implies that each spawned thread can be context switched a fixed constant number of times. Our proof is technical, since fair termination requires reasoning about the composition of unboundedly many threads each with unboundedly large stacks. In fact, techniques for related problems, which depend crucially on replacing the pushdown threads with finite-state threads, are not applicable. Instead, we introduce an extension of vector addition systems with states (VASS), called VASS with balloons (VASSB), as an intermediate model; it is an infinite-state model of independent interest. A VASSB allows tokens that are themselves markings (balloons). We show that context bounded fair termination reduces to fair termination for VASSB. We show the latter problem is decidable by showing a series of reductions: from fair termination to configuration reachability for VASSB and thence to the reachability problem for VASS. For a lower bound, fair termination is known to be non-elementary already in the special case where threads run to completion (no context switches). We also show that the simpler problem of context-bounded termination is 2EXPSPACE-complete, matching the complexity bound---and indeed the techniques---for safety verification. Additionally, we show the related problem of fair starvation, which checks if some thread can be starved along a fair run, is also decidable in the context-bounded case. The decidability employs an intricate reduction from fair starvation to fair termination. Like fair termination, this problem is also non-elementary.

International audience; We show that model-checking flat counter systems with the branching-time temporal logic CTL* extended with arithmetical constraints on counter values has the same worst-case complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with strong restrictions: the logical language uses only the temporal operator EF and no arithmetical constraints, and the guards on the transitions are made of linear constraints. This work complements our understanding of model-checking flat counter systems with linear-time temporal logics, such as LTL, for which the problem is already known to be (only) NP-complete with guards restricted to the linear fragment.

The reachability problem is one of the most important issues in the verification of hybrid systems. But unfortunately the reachable sets for most of hybrid systems are not computable. In the literature, only some special families of linear vector fields are proved with decidable reachability problem, let alone nonlinear ones. In this paper, we investigate the reachability problem of nonlinear vector fields by identifying three families of nonlinear vector fields with solvability and prove that their reachability problems are decidable. An $n$ -dimension dynamical system is called solvable if its state variables can be partitioned into $m$ groups such that the derivatives of the variables in the $i$ th group are linear in themselves, but possibly nonlinear in the variables from the 1st to $i-1$ th groups. The three families of nonlinear solvable vector fields under consideration are: the matrices corresponding to the linear parts of any vector field in the first family are nilpotent; the matrices corresponding to the linear parts of any vector in the second family are only with real eigenvalues; the matrices corresponding to the linear parts of any vector field in the third family are only with pure imaginary eigenvalues. The experimental results indicate the efficiency of our approach.

International audience; In this article we introduce the problem of timed pattern diagnosis in timed system and propose a method to solve a sub-class of theses problems: the problem of timed pattern diagnosis of workflows. It consists in searching for all the possible evolutions of the workflow that are consistent with a timed sequence of observations and determining whether these evolutions match a pattern of timed events instead of a single fault event. The formal characterization of the diagnosis problem is based on the notion of pattern matching. Defined as a reachability problem, the diagnosis problem is then solved by model checking.

Given a graph G and two vertices s and t in it, graph reachability is the problem of checking whether there exists a path from s to t in G . We show that reachability in directed layered planar graphs can be decided in polynomial time and O ( n ϵ ) space, for any ϵ > 0. The previous best-known space bound for this problem with polynomial time was approximately O (√ n ) space (Imai et al. 2013). Deciding graph reachability in SC (Steve's class) is an important open question in complexity theory, and in this article, we make progress toward resolving this question.

Action planning deals with the problem of finding a sequence of actions transferring the world from a given state to a desired (goal) state. This problem is important in various areas such as robotics, manufacturing, transportation, autonomic computing, computer games, etc. Action planning is a form of a reachability problem in a huge state space so it is critical to efficiently represent world states and actions (transitions between states). In this paper we present a modeling framework for planning problems based on tabled logic programming that exploits a planner module in the Picat language. In particular, we suggest techniques for structured representation of states and for including control knowledge in the description of actions. We demonstrate these techniques using the complex planning domain Cave Diving from the International Planning Competition. Experimentally, we show properties of the model for different search approaches and we compare the performance of the proposed approach with state-of-the-art automated planners. The focus of this paper is on providing guidelines for manual modeling of planning domains rather than on automated reformulation of models.

Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with a novel attack that can be carried out on most Distance Bounding Protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We additionally present a probabilistic analysis of this novel attack. As a formal model for representing and analyzing Cyber-Physical properties, we propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model, and show that for the important class of balanced theories the reachability problem is PSPACE-complete. We also show how our model can be implemented using the computational rewriting tool Maude, the machinery that automatically searches for such attacks., Comment: Extending our POST 2015 paper

This work studies the relationship between verifiable and computable answers for reachability problems in rewrite theories with an underlying membership equational logic. A new definition for R, A-rewriting that allows us to solve a bigger class of reachability problems, and a calculus that solves this class of problems always working with canonical terms and normalized substitutions has been developed. Given a reachability problem in a rewrite theory, this calculus can compute any normalized answer that can be checked by rewriting, or a more general one that can be instantiated to that answer.

We consider the problem of reachability in pushdown graphs. We study the problem for pushdown graphs with constant treewidth. Even for pushdown graphs with treewidth 1, for the reachability problem we establish the following: (i) the problem is PTIME-complete, and (ii) any subcubic algorithm for the problem would contradict the k-clique conjecture and imply faster combinatorial algorithms for cliques in graphs. The study of reachability in pushdown systems with constant treewidth restriction.We show the problem remains PTIME-complete even for treewidth 1.We show better algorithms for treewidth 1 imply the same for cliques in graphs.