Search

We describe a new technique for computing procedure summaries for performing an interprocedural analysis on programs. Procedure summaries are computed by performing a backward analysis of procedures, but there are two key new features: (i) information is propagated using "generic" assertions (rather than regular assertions that are used in intraprocedural analysis); and (ii) unification is used to simplify these generic assertions. We illustrate this general technique by applying it to two abstractions: unary uninterpreted functions and linear arithmetic. In the first case, we get a PTIME algorithm for a special case of the long-standing open problem of interprocedural global value numbering (the special case being that we consider unary uninterpreted functions instead of binary). This also requires developing efficient algorithms for manipulating singleton context-free grammars, and builds on an earlier work by Plandowski [13]. In linear arithmetic case, we get new algorithms for precise interprocedural analysis of linear arithmetic programs with complexity matching that of the best known deterministic algorithm [11]. [ABSTRACT FROM AUTHOR]

Termination and innermost termination are shown to be decidable for term rewrite systems whose right-hand side terms are restricted to be shallow (variables occur at depth at most one) and linear. Innermost termination is also shown to be decidable for shallow rewrite systems. In all cases, we show that nontermination implies nontermination starting from flat terms. The proof is completed by using the useful enabling result that, for right shallow rewrite systems, existence of nonterminating derivations starting from a given term is decidable. We also show that termination is undecidable for shallow rewrite systems. For right-shallow systems, general and innermost termination are both undecidable. [ABSTRACT FROM AUTHOR]

This paper presents the foundations for using automated deduction technology in static program analysis. The central principle is the use of logical lattices - a class of lattices defined on logical formulas in a logical theory - in an abstract interpretation framework. Abstract interpretation over logical lattices, called logical interpretation, raises new challenges for theorem proving. We present an overview of some of the existing results in the field of logical interpretation and outline some requirements for building expressive and scalable logical interpreters. [ABSTRACT FROM AUTHOR]

We describe an abstract domain for representing useful invariants of heap-manipulating programs (in presence of recursive data structures and pointer arithmetic) written in languages like C or low-level code. This abstract domain allows representation of must and may equalities among pointer expressions. Pointer expressions contain existentially or universally quantified integer variables guarded by some base domain constraint. We allow quantification of a special form, namely $\exists \forall$ quantification, to balance expressiveness with efficient automated deduction. The existential quantification is over some dummy non-program variables, which are automatically made explicit by our analysis to express useful program invariants. The universal quantifier is used to express properties of collections of memory locations. Our abstract interpreter automatically computes invariants about programs over this abstract domain. We present initial experimental results demonstrating the effectiveness of this abstract domain on some common coding patterns. [ABSTRACT FROM AUTHOR]

We revisit the connection between equality assertion checking in programs and unification that was recently described in [7]. Using a general formalization of this connection, we establish interesting connections between the complexity of assertion checking in programs and unification theory of the underlying program expressions. In particular, we show that assertion checking is: (a) PTIME for programs with nondeterministic conditionals that use expressions from a strict unitary theory, (b) coNP-hard for programs with nondeterministic conditionals that use expressions from a bitary theory, and (c) decidable for programs with disequality guards that use expressions from a convex finitary theory. These results generalize several recently published results and also establish several new results. In essence, they provide new techniques for backward analysis of programs based on novel integration of theorem proving technology in program analysis. [ABSTRACT FROM AUTHOR]

This paper presents results on the problem of checking equality assertions in programs whose expressions have been abstracted using combination of linear arithmetic and uninterpreted functions, and whose conditionals are treated as non-deterministic. We first show that the problem of assertion checking for this combined abstraction is coNP-hard, even for loop-free programs. This result is quite surprising since assertion checking for the individual abstractions of linear arithmetic and uninterpreted functions can be performed efficiently in polynomial time. Next, we give an assertion checking algorithm for this combined abstraction, thereby proving decidability of this problem despite the underlying lattice having infinite height. Our algorithm is based on an important connection between unification theory and program analysis. Specifically, we show that weakest preconditions can be strengthened by replacing equalities by their unifiers, without losing any precision, during backward analysis of programs. [ABSTRACT FROM AUTHOR]

In [1] we advocated the need for an interchange format for hybrid systems that enables the integration of design tools coming from many different research communities. In deriving such interchange format the main challenge is to define a language that, while presenting a particular formal semantics, remains general enough to accommodate the translation across the various modeling approaches used in the existing tools. In this paper we give a formal definition of the syntax and semantics for the proposed interchange format. In doing so, we clearly separate the structure of a hybrid system from the semantics attached to it. The semantics can be considered an "abstract semantics" in the sense that it can be refined to yield the model of computation, or "concrete semantics", which, in turn, is associated to the existing languages that are used to specify hybrid systems. We show how the interchange format can be used to capture the essential information across different modeling approaches and how such information can be used in the translation process. [ABSTRACT FROM AUTHOR]

Finite plans proved to be an efficient method to steer complex control systems via feedback quantization. Such finite plans can be encoded by finite-length words constructed on suitable alphabets, thus permitting transmission on limited capacity channels. In particular flat systems can be steered computing arbitrarily close approximations of a desired equilibrium in polynomial time. The paper investigates how the efficiency of planning is affected by the choice of inputs, and provides some results as to optimal performance in terms of accuracy and range. Efficiency is here measured in terms of computational complexity and description length (in number of bits) of finite plans. [ABSTRACT FROM AUTHOR]

Verification and simulation have always been complementary, if not competing, approaches to system design. In this paper, we present a novel method for so-called metric transition systems that bridges the gap between verification and simulation, enabling system verification using a finite number of simulations. The existence of metrics on the system state and observation spaces, which is natural for continuous systems, allows us to capitalize on the recently developed framework of approximate bisimulations, and infer the behavior of neighborhood of system trajectories around a simulated trajectory. For nondeterministic linear systems that are robustly safe or robustly unsafe, we provide not only a completeness result but also an upper bound on the number of simulations required as a function of the distance between the reachable set and the unsafe set. Our framework is the first simulation-based verification method that enjoys completeness for infinite-state systems. The complexity is low for robustly safe or robustly unsafe systems, and increases for nonrobust problems. This provides strong evidence that robustness dramatically impacts the complexity of system verification and design. [ABSTRACT FROM AUTHOR]

In this paper we propose a technique to extend the simulation of a Zeno hybrid system beyond its Zeno time point. A Zeno hybrid system model is a hybrid system with an execution that takes an infinite number of discrete transitions during a finite time interval. We argue that the presence of Zeno behavior indicates that the hybrid system model is incomplete by considering some classical Zeno models that incompletely describe the dynamics of the system being modeled. This motivates the systematic development of a method for completing hybrid system models through the introduction of new post-Zeno states, where the completed hybrid system transitions to these post-Zeno states at the Zeno time point. In practice, simulating a Zeno hybrid system is challenging in that simulation effectively halts near the Zeno time point. Moreover, due to unavoidable numerical errors, it is not practical to exactly simulate a Zeno hybrid system. Therefore, we propose a method for constructing approximations of Zeno models by leveraging the completed hybrid system model. Using these approximation, we can simulate a Zeno hybrid system model beyond its Zeno point and reveal the complete dynamics of the system being modeled. [ABSTRACT FROM AUTHOR]

This article proves the existence and uniqueness of a weak solution to a scalar conservation law on a bounded domain. A weak formulation of hybrid boundary conditions is needed for the problem to be well posed. The boundary conditions are represented by a hybrid automaton with switches between the modes determined by the direction of characteristics of the system at the boundary. The existence of the solution results from the convergence of a Godunov scheme derived in this article. This weak formulation is written explicitly in the context of a strictly concave flux function (relevant for highway traffic). The numerical scheme is then applied to a highway scenario with data from the I210 highway obtained from the California PeMS system. Finally, the existence of a minimizer of travel time is obtained, with the corresponding optimal boundary control. Keywords: Weak solution of scalar conservation laws, Weak hybrid boundary conditions, LWR PDE, Highway traffic modeling, Boundary control. [ABSTRACT FROM AUTHOR]

We investigate techniques for automatically generating symbolic approximations to the time solution of a system of differential equations. This is an important primitive operation for the safety analysis of continuous and hybrid systems. In this paper we design a time elapse operator that computes a symbolic over-approximation of time solutions to a continuous system starting from a given initial region. Our approach is iterative over the cone of functions (drawn from a suitable universe) that are non negative over the initial region. At each stage, we iteratively remove functions from the cone whose Lie derivatives do not lie inside the current iterate. If the iteration converges, the set of states defined by the final iterate is shown to contain all the time successors of the initial region. The convergence of the iteration can be forced using abstract interpretation operations such as widening and narrowing. We instantiate our technique to linear hybrid systems with piecewise-affine dynamics to compute polyhedral approximations to the time successors. Using our prototype implementation , we demonstrate the performance of our technique on benchmark examples. [ABSTRACT FROM AUTHOR]

Several recent results in the area of robust asymptotic stability of hybrid systems show that the concept of a generalized solution to a hybrid system is suitable for the analysis and design of hybrid control systems. In this paper, we show that such generalized solutions are exactly the solutions that arise when measurement noise is present in the system. [ABSTRACT FROM AUTHOR]

We call a hybrid system stable if every trajectory inevitably ends up in a given region. Our notion of stability deviates from classical definitions in control theory. In this paper, we present a model checking algorithm for stability in the new sense. The idea of the algorithm is to reduce the stability proof for the whole system to a set of (smaller) proofs for several one-mode systems. [ABSTRACT FROM AUTHOR]

A switched system is a hybrid system whose discrete mechanisms are abstracted away in terms of an exogenous switching signal which brings about the mode switches. For switched systems, the Average Dwell time (ADT) property defines restricted classes of switching signals which can be used for proving stability. In this paper, we develop optimization-based methods for automatically verifying ADT properties of hybrid systems. This enables us to prove stability of hybrid systems, provided the individual modes of the system are stable. For two special classes of hybrid systems, we show that the resulting optimization problems can indeed be solved efficiently using standard mathematical programming techniques. We also present simulation relation-based proof methods for establishing equivalence of hybrid systems with respect to ADT. The proposed methods are applied to verify ADT properties of a linear hysteresis switch and a nondeterministic thermostat. [ABSTRACT FROM AUTHOR]

In practice, many stochastic hybrid systems are not autonomous: they are objects that communicate with other objects by exchanging messages through an asynchronous medium such as a network. Issues such as: how to compositionally specify distributed object-based stochastic hybrid systems (OBSHS), how to formally model them, and how to verify their properties seem therefore quite important. This paper addresses these issues by: (i) defining a mathematical model for such systems that can be naturally regarded as a generalized stochastic hybrid system (GSHS) in the sense of [6]; (ii) proposing a formal OBSHS specification language in which system transitions are specified in a modular way by probabilistic rewrite rules; and (iii) showing how these systems can be subjected to statistical model checking analysis to verify their probabilistic temporal logic properties. [ABSTRACT FROM AUTHOR]

In this paper, we show that the finite gain (FG) lp stabilization, with 1 ≤ p ≤ ∞, of a discrete-time, linear and time-invariant unstable plant is impossible by bit rate constrained feedback. In addition, we show that, under bit rate constrained feedback, weaker (local) versions of FG lp stability are also impossible. These facts are not obvious, since recent results have shown that input to state stabilization (ISS) is viable by bit-rate constrained control. We establish a comparison with existing work, leading to two conclusions: (1) in spite of ISS stability being attainable under bit rate constrained feedback, small changes in the amplitude of the external excitation may cause, in relative terms, a large increase in the amplitude of the state (2) FG lp stabilization requires logarithmic precision around zero, implying that even without bit-rate constraints FG lp stabilization is impossible in practice. Since our conclusions hold with no assumptions on the feedback structure, they cannot be derived from existing results. We adopt an information theoretic viewpoint, which also brings new insights into the problem of stabilization. [ABSTRACT FROM AUTHOR]

In this paper we will investigate a stochastic hybrid delay population dynamics (SHDPD) and show under certain conditions, the SHDPD will have global positive solution. Ultimate boundedness and extinction, two important properties in a population systems, are discussed. Keywords: Brownian motion, Itô's formula, ultimate boundedness, extinction. [ABSTRACT FROM AUTHOR]

We present a general approach to analyzing stability of hybrid systems, based on input-to-state stability (ISS) and small-gain theorems. We demonstrate that the ISS small-gain analysis framework is very naturally applicable in the context of hybrid systems. Novel Lyapunov-based and LaSalle-based small-gain theorems for hybrid systems are presented. The reader does not need to be familiar with ISS or small-gain theorems to be able to follow the paper. [ABSTRACT FROM AUTHOR]

Monitoring a hybrid system subjected to human actions needs both an estimation of the system state and an analysis of the possible conflicts in order to guarantee a safe behavior of the system. Such a monitoring principle is presented in this paper. The estimation of the hybrid system state is performed using the particle Petri net model. Then the estimated state is analysed by checking its consistency with respect to the reachable markings of the Petri net. The principle is applied to aircraft pilot's activity tracking and conflict detection. [ABSTRACT FROM AUTHOR]

This paper describes the modeling language as an extension for architectural reconfiguration to the existing distributed hybrid system modeling language Charon. The target application domain of includes but is not limited to modular reconfigurable robots and large-scale transportation systems. While largely leaving the Charon syntax and semantics intact, allows dynamic creation and destruction of components (agents) as well as of links (references) between the agents. As such, is the first formal, hybrid automata based modeling language which also addresses dynamic reconfiguration. We develop and present the syntax and operational semantics for on three levels: behavior (modes), structure (agents) and configuration (system). [ABSTRACT FROM AUTHOR]

Stochastic hybrid system models can be used to analyze and design complex embedded systems that operate in the presence of uncertainty and variability. Verification of reachability properties for such systems is a critical problem. Developing algorithms for reachability analysis is challenging because of the interaction between the discrete and continuous stochastic dynamics. In this paper, we propose a probabilistic method for reachability analysis based on discrete approximations. The contribution of the paper is twofold. First, we show that reachability can be characterized as a viscosity solution of a system of coupled Hamilton-Jacobi-Bellman equations. Second, we present a numerical method for computing the solution based on discrete approximations and we show that this solution converges to the one for the original system as the discretization becomes finer. Finally, we illustrate the approach with a navigation benchmark that has been proposed for hybrid system verification. [ABSTRACT FROM AUTHOR]

This paper addresses the question of extending the usual approximation and sampling theory of continuous signals and systems to those encompassing discontinuities, such as found in modern distributed control systems. We provide a topological framework dealing with continuous, discrete and mixed systems in a uniform manner. We show how this theoretical framework can be used for voting on hybrid signals in critical real-time systems. [ABSTRACT FROM AUTHOR]

We present a technique for reachability analysis of continuous multi-affine systems based on rectangular partitions. The method is iterative. At each step, finer partitions and larger discrete quotients are produced. We exploit some interesting convexity properties of multi-affine functions on rectangles to show that the construction of the discrete quotient at each step requires only the evaluation of the vector field at the set of all vertices of all rectangles in the partition and finding the roots of a finite set of scalar affine functions. The methodology promises to be easily extendable to rectangular hybrid automata with multi-affine vector fields and is expected to find important applications in analysis of biological networks and robot control. [ABSTRACT FROM AUTHOR]

We consider the following problem: given a linear system and an LTL-X formula over a set of linear predicates in its state variables, find a feedback control law with polyhedral bounds and a set of initial states so that all trajectories of the closed loop system satisfy the formula. Our solution to this problem consists of three main steps. First, we partition the state space in accordance with the predicates in the formula and construct a transition system over the partition quotient, which captures our capability of designing controllers. Second, using model checking, we determine runs of the transition system satisfying the formula. Third, we generate the control strategy. Illustrative examples are included. [ABSTRACT FROM AUTHOR]

This paper discusses a notion of approximate abstraction for linear stochastic hybrid automata (LSHA). The idea is based on the construction of the so called stochastic bisimulation function. Such function can be used to quantify the distance between a system and its approximate abstraction. The work in this paper generalizes our earlier work for jump linear stochastic systems (JLSS). In this paper we demonstrate that linear stochastic hybrid automata can be cast as a modified JLSS and modify the procedure for constructing the stochastic bisimulation function accordingly. The construction of quadratic stochastic bisimulation functions is essentially a linear matrix inequality problem. In this paper, we also discuss possible extensions of the framework to handle nonlinear dynamics and variable rate Poisson processes. As an example, we apply the framework to a chain-like stochastic hybrid automaton. [ABSTRACT FROM AUTHOR]

This paper addresses the receding horizon control problem of continuous-time linear systems with respect to continuous control inputs and discrete state waypoints under discrete-dynamical constraints. First, a generalized version of our previous method is described, where a discretization technique is applied only for the constrained state variables. Next, it is proven that the problem is reduced to the finite-time optimal control problem of a certain discrete-time linear system with discrete-valued inputs. Finally, a new efficient algorithm for solving this optimization problem is proposed. Several numerical simulations show that this solver is much faster than the CPLEX solver. [ABSTRACT FROM AUTHOR]

This paper presents a method for computing the reach set of affine systems for sets of initial states given as low-dimensional polytopes. An affine representation for polytopes is introduced to improve the efficiency of set representations. Using the affine representation, we present a procedure to compute conservative over-approximations of the reach set, which uses the Krylov subspace approximation method to handle large-scale affine systems (systems of order over 100). [ABSTRACT FROM AUTHOR]

A general Hybrid Minimum Principle (HMP) for hybrid optimal control problems (HOCPs) is presented in [1, 2, 3, 4] and in [4, 5], a class of efficient, provably convergent Hybrid Minimum Principle (HMP) algorithms were obtained based upon the HMP. The notion of optimality zones (OZs) ([3, 4]) provides a theoretical framework for the computation of optimal location (i.e. discrete state) schedules for HOCPs (i.e. discrete state sequences with the associated switching times and states). This paper presents the algorithm HMPOZ which fully integrates the prior computation of the OZs into the HMP algorithms class. Summing (a) the computational investment in the construction of the OZs for a given HOCP, and (b) the complexity of (i) the computation of the optimal schedule, (ii) the optimal switching time and optimal switching state sequence, and (iii) the optimal continuous control input, yields a complexity estimate for the algorithm HMPOZ which is linear (i.e. O(L)) in the number of switching times L. [ABSTRACT FROM AUTHOR]

This work is concerned with the problem of computing the set of reachable states for linear time-invariant systems with bounded inputs. Our main contribution is a novel algorithm which improves significantly the computational complexity of reachability analysis. Algorithms to compute over and under-approximations of the reachable sets are proposed as well. These algorithms are not subject to the wrapping effect and therefore our approximations are tight. We show that these approximations are useful in the context of hybrid systems verification and control synthesis. The performance of a prototype implementation of the algorithm confirms its qualities and gives hope for scaling up verification technology for continuous and hybrid systems. [ABSTRACT FROM AUTHOR]

We revisit the problem of designing controllers to meet safety specifications for hybrid systems, whose evolution is affected by both control and disturbance inputs. The problem is formulated as a dynamic game and an appropriate notion of hybrid strategy for the control inputs is developed. The design of hybrid strategies to meet safety specifications is based on an iteration of alternating discrete and continuous safety calculations. We show that, under certain assumptions, the iteration converges to a fixed point, which turns out to be the maximal set of states for which the safety specifications can be met. The continuous part of the calculation relies on the computation of the set of winning states for one player in a two player, two target, pursuit evasion differential game. We develop a characterization of these winning states using methods from non-smooth analysis and viability theory. [ABSTRACT FROM AUTHOR]

We present a new method to solve the constrained finite-time optimal control (CFTOC) problem for piece-wise polynomial (PWP) hybrid systems, based on Cylindrical Algebraic Decomposition (CAD). The computational approach consists of two parts. The off-line, where the method re-formulates the original CFTOC optimization problem in algebraic form, decomposes it into smaller subproblems and then independently pre-processes each subproblem to obtain certain structural information, and the on-line, where this available precomputed information is used to efficiently compute the optimal solution of the original problem in real time. The method is illustrated through its application to the control of a boost dc-dc converter. [ABSTRACT FROM AUTHOR]

The problem of driving a collection of mobile robots to a given target location is studied in the context of partial difference equations. In particular, we are interested in achieving this transfer while ensuring that the agents stay in the convex polytope spanned by dedicated leader-agents, whose dynamics will be given by a hybrid Stop-Go policy. The resulting system ensures containment through the enabling result that under a Laplacian, decentralized control strategy for the followers, these followers will converge to a location in the convex leader polytope, as long as the leaders are stationary and the interaction graph is connected. Simulation results testify to the viability of the proposed, hybrid control strategy. [ABSTRACT FROM AUTHOR]

We study two questions in the theory of timed automata concerning timed language inclusion of real-time programs modeled as timed pushdown automata in real-time specifications with just one clock. We show that if the specification B is modeled as a timed automaton with one clock, then the language inclusion problem for a timed pushdown automaton A is decidable. On the other hand, we show that the universality problem of timed visibly pushdown automata with only one clock is undecidable. Thus there is no algorithm to check language inclusion of real-time programs for specifications given by visibly pushdown specifications with just one clock. [ABSTRACT FROM AUTHOR]

Recent advances of experimental techniques in biology have led to the production of enormous amounts of data on the dynamics of genetic regulatory networks. In this paper, we present an approach for the identification of PieceWise-Affine (PWA) models of genetic regulatory networks from experimental data, focusing on the reconstruction of switching thresholds associated with regulatory interactions. In particular, our method takes into account geometric constraints specific to models of genetic regulatory networks. We show the feasibility of our approach by the reconstruction of switching thresholds in a PWA model of the carbon starvation response in the bacterium Escherichia coli. [ABSTRACT FROM AUTHOR]

In this paper, we deal with the observability problem of a class of Hybrid Systems whose output is a timed string on a finite alphabet. We determine under which conditions it is always possible to immediately detect, using the observed output, when the system enters a given discrete state. We illustrate how to construct a Timed Automaton that is an abstraction of the given Hybrid System, and that preserves its observability properties. Moreover, we propose a verification algorithm with polynomial complexity for checking the observability of the Timed Automaton, and a constructive procedure for an observer of the discrete state. [ABSTRACT FROM AUTHOR]

In this paper, we propose a fixed point theory to solve games of imperfect information. The fixed point theory is defined on the lattice of antichains of sets of states. Contrary to the classical solution proposed by Reif [Rei84], our new solution does not involve determinization. As a consequence, it is readily applicable to classes of systems that do not admit determinization. Notable examples of such systems are timed and hybrid automata. As an application, we show that the discrete control problem for games of imperfect information defined by rectangular automata is decidable. This result extends a result by Henzinger and Kopke in [HK99]. [ABSTRACT FROM AUTHOR]

In this paper we propose an algorithm for approximating the reachable sets of systems defined by polynomial differential equations. Such systems can be used to model a variety of physical phenomena. We first derive an integration scheme that approximates the state reachable in one time step by applying some polynomial map to the current state. In order to use this scheme to compute all the states reachable by the system starting from some initial set, we then consider the problem of computing the image of a set by a multivariate polynomial. We propose a method to do so using the Bézier control net of the polynomial map and the blossoming technique to compute this control net. We also prove that our overall method is of order 2. In addition, we have successfully applied our reachability algorithm to two models of a biological system. [ABSTRACT FROM AUTHOR]

We present an industrial case study in automotive control of significant complexity: the new common rail fuel injection system for Diesel engines, currently under production by Magneti Marelli Powertrain. In this system, a flow-rate valve, introduced before the High Pressure (HP) pump, regulates the fuel flow that supplies the common rail according to the engine operating point. The standard approach followed in automotive control is to use a mean-value model for the plant and to develop a controller based on this model. In this particular case, this approach does not provide a satisfactory solution as the discrete-continuous interactions in the fuel injection system, due to the slow time-varying frequency of the HP pump cycles and the fast sampling frequency of sensing and actuation, play a fundamental role. We present a design approach based on a hybrid model of the Magneti Marelli Powertrain common-rail fuel-injection system for four-cylinder multi-jet engines and a hybrid approach to the design of a rail pressure controller. The hybrid controller is compared with a classical mean-value based approach to automotive control design whereby the quality of the hybrid solution is demonstrated. [ABSTRACT FROM AUTHOR]

This paper proposes an event-driven model predictive control scheme with guaranteed closed-loop convergence properties for the class of integral continuous-time hybrid automata (icHA). After converting icHA to a corresponding event-driven representation that allows one to compute the model predictive control action by mixed integer programming, sufficient conditions ensuring event-asymptotic and time-asymptotic convergence are proven. The paper also shows how the same modeling methodology can be employed to efficiently solve problems of verification of safety properties. [ABSTRACT FROM AUTHOR]

Optimal switch-time control is an area that investigates how best to switch between different control modes. In this paper we present an algorithm for solving the optimal switch-time control problem for nonlinear systems where the state is only partially known through the outputs. A method is presented that both guarantees that the current switch-time estimates remain optimal as the state estimates evolve, and that ensures this in a computationally feasible manner, thus rendering the method applicable to real-time applications. The viability of the proposed method is illustrated through a number of examples. [ABSTRACT FROM AUTHOR]

A model for discrete time stochastic hybrid systems whose evolution can be influenced by some control input is proposed in this paper. With reference to the introduced class of systems, a methodology for probabilistic reachability analysis is developed that is relevant to safety verification. This methodology is based on the interpretation of the safety verification problem as an optimal control problem for a certain controlled Markov process. In particular, this allows to characterize through some optimal cost function the set of initial conditions for the system such that safety is guaranteed with sufficiently high probability. The proposed methodology is applied to the problem of regulating the average temperature in a room by a thermostat controlling a heater. [ABSTRACT FROM AUTHOR]

Model checking is a popular algorithmic verification technique for checking temporal requirements of mathematical models of systems. In this paper, we consider the problem of verifying bounded reachability properties of stochastic real-time systems modeled as generalized semi-Markov processes (GSMP). While GSMPs is a rich model for stochastic systems widely used in performance evaluation, existing model checking algorithms are applicable only to subclasses such as discrete-time or continuous-time Markov chains. The main contribution of the paper is an algorithm to compute the probability that a given GSMP satisfies a property of the form "can the system reach a target before time T within k discrete events, while staying within a set of safe states". For this, we show that the probability density function for the remaining firing times of different events in a GSMP after k discrete events can be effectively partitioned into finitely many regions and represented by exponentials and polynomials. We report on illustrative examples and their analysis using our techniques. [ABSTRACT FROM AUTHOR]

Zeno behaviors are one of the (perhaps unintended) features of many hybrid models of physical systems. They have no counterpart in traditional dynamical systems or automata theory and yet they have remained relatively unexplored over the years. In this paper we address the stability properties of a class of Zeno equilibria, and we introduce a necessary paradigm shift in the study of hybrid stability. Motivated by the peculiarities of Zeno equilibria, we consider a form of asymptotic stability that is global in the continuous state, but local in the discrete state. We provide sufficient conditions for stability of these equilibria, resulting in sufficient conditions for the existence of Zeno behavior. [ABSTRACT FROM AUTHOR]

We show the regularity of the discrete time behaviour of hybrid automata in which the rates of continuous variables are governed by linear differential operators in a diagonal form and in which the values of the continuous variables can be observed only with finite precision. We do not demand resetting of the values of the continuous variables during mode changes. We can cope with polynomial guards and we can tolerate bounded delays both in sampling the values of the continuous variables and in effecting changes in their rates required by mode switchings. We also show that if the rates are governed by diagonalizable linear differential operators with rational eigenvalues and there is no delay in effecting rate changes, the discrete time behaviour of the hybrid automaton is recursive. However, the control state reachability problem in this setting is undecidable. [ABSTRACT FROM AUTHOR]