Search results for "Reachability"
showing 10 items of 17 documents
Relative Reachability Analysis as a Tool for Urban Mobility Planning
2019
There is a plethora of user-oriented route planning applications and systems that enable the computation of the fastest journey between two locations using different transportation modes, e.g., car, public transport, walking, bicycle. While useful for individuals, they are of limited interest to a class of users that may be interested in a more global and comparative view of transportation systems in general. In this context, we adopt the view of an urban planner. Urban planners may be interested in queries such as "if a new transit stop was to be introduced in a given location, would that bring the travel time to a given point-of-interest (POI) or area-of-interest (AOI) by bus closer to th…
Modular Strategies for Recursive Game Graphs
2006
AbstractMany problems in formal verification and program analysis can be formalized as computing winning strategies for two-player games on graphs. In this paper, we focus on solving games in recursive game graphs which can model the control flow in sequential programs with recursive procedure calls. While such games can be viewed as the pushdown games studied in the literature, the natural notion of winning in our framework requires the strategies to be modular with only local memory; that is, resolution of choices within a module does not depend on the context in which the module is invoked, but only on the history within the current invocation of the module. While reachability in (global…
Decidability of bisimulation equivalences for parallel timer processes
1993
In this paper an abstract model of parallel timer processes (PTPs), allowing specification of temporal quantitative constraints on the behaviour of real time systems, is introduced. The parallel timer processes are defined in a dense time domain and are able to model both concurrent (with delay intervals overlapping on the time axis) and infinite behaviour. Both the strong and weak (abstracted from internal actions) bisimulation equivalence problems for PTPs are proved decidable. It is proved also that, if one provides the PTP model additionally with memory cells for moving timer value information along the time axis, the bisimulation equivalence (and even the vertex reachability) problems …
Varieties and Covarieties of Languages (Extended Abstract)
2013
AbstractBecause of the isomorphism (X×A)→X≅X→(A→X), the transition structure of a deterministic automaton with state set X and with inputs from an alphabet A can be viewed both as an algebra and as a coalgebra. This algebra-coalgebra duality goes back to Arbib and Manes, who formulated it as a duality between reachability and observability, and is ultimately based on Kalmanʼs duality in systems theory between controllability and observability. Recently, it was used to give a new proof of Brzozowskiʼs minimization algorithm for deterministic automata. Here we will use the algebra-coalgebra duality of automata as a common perspective for the study of both varieties and covarieties, which are …
Optimal paths in weighted timed automata
2004
AbstractWe consider the optimal-reachability problem for a timed automaton with respect to a linear cost function which results in a weighted timed automaton. Our solution to this optimization problem consists of reducing it to computing (parametric) shortest paths in a finite weighted directed graph. We call this graph a parametric sub-region graph. It refines the region graph, a standard tool for the analysis of timed automata, by adding the information which is relevant to solving the optimal-reachability problem. We present an algorithm to solve the optimal-reachability problem for weighted timed automata that takes time exponential in O(n(|δ(A)|+|wmax|)), where n is the number of clock…
Deciding reachability for planar multi-polynomial systems
1996
In this paper we investigate the decidability of the reachability problem for planar non-linear hybrid systems. A planar hybrid system has the property that its state space corresponds to the standard Euclidean plane, which is partitioned into a finite number of (polyhedral) regions. To each of these regions is assigned some vector field which governs the dynamical behaviour of the system within this region. We prove the decidability of point to point and region to region reachability problems for planar hybrid systems for the case when trajectories within the regions can be described by polynomials of arbitrary degree.
General decidability theorems for infinite-state systems
2002
Over the last few years there has been an increasing research effort directed towards the automatic verification of infinite state systems. This paper is concerned with identifying general mathematical structures which can serve as sufficient conditions for achieving decidability. We present decidability results for a class of systems (called well-structured systems), which consist of a finite control part operating on an infinite data domain. The results assume that the data domain is equipped with a well-ordered and well-founded preorder such that the transition relation is "monotonic" (is a simulation) with respect to the preorder. We show that the following properties are decidable for …
Robust control of stochastic systems against bounded disturbances with application to flight control
2014
This paper investigates the problems of state observer design and observer-based integral sliding-mode control (SMC) for a class of Itô stochastic systems subject to simultaneous input and output disturbances. A new type of sliding-mode-based descriptor observer method is developed to approximate the system state and disturbance vectors. An integral-type SMC scheme is proposed based on the state estimation to stabilize the overall system. The main contributions of this approach are as follows: 1) The desired estimations of state and disturbance vectors can be obtained simultaneously, and 2) in the designed sliding-mode observer, the integral term of the Itô stochastic noise is eliminated …
A study of mobility and reachability in ad hoc networks using stochastic activity networks
2006
The integration of ad-hoc networks into real environments is now becoming more and more common and supervision and control systems are no exception. The efficiency of the communication in these networks as well as various other factors, are governed by the working area, the number of nodes, mobility, transmission power, etc. In this paper, the mobility and reachability of mobile nodes appearing spontaneously in a large installation such as can be found in a water purification system are studied. These nodes form an ad-hoc network and communicate between each other in order to finally reach a fixed node which can offer them information from the rest of the system in real time or act as a gat…
Finite automata on timed ω-trees
2003
AbstractIn the last decade Alur and Dill introduced a model of automata on timed ω-sequences which extends the traditional models of finite automata. In this paper, we present a theory of timed ω-trees which extends both the theory of timed ω-sequences and the theory of ω-trees. The main motivation is to introduce a new way of specifying real-time systems and provide tools for studying decidability problems in related fields. We focus on the decision problems and their applications in system verification and synthesis.