IEEE Transactions on Automatic Control · 2007 · 485 citations · 15 references
ComputingComputer ScienceSystems EngineeringAlgorithmsCyber-physical SystemsTheory Of ComputationApproximation AlgorithmsConcurrent ModelingConcurrent System VerificationHybrid SystemsHybrid Systems VerificationModel CheckingBisimulationBisimulation AnalysisDiscrete-event SystemsExact AlgorithmsFinite-state VerificationLyapunov FunctionsMetricsSafety Verification
Established system relationships for discrete systems, such as language inclusion, simulation, and bisimulation, require system observations to be identical. When interacting with the physical world, modeled by continuous or hybrid systems, exact relationships are restrictive and not robust. In this paper, we develop the first framework of system approximation that applies to both discrete and continuous systems by developing notions of approximate language inclusion, approximate simulation, and approximate bisimulation relations. We define a hierarchy of approximation pseudo-metrics between two systems that quantify the quality of the approximation, and capture the established exact relationships as zero sections. Our approximation framework is compositional for a synchronous composition operator. Algorithms are developed for computing the proposed pseudo-metrics, both exactly and approximately. The exact algorithms require the generalization of the fixed point algorithms for computing simulation and bisimulation relations, or dually, the solution of a static game whose cost is the so-called branching distance between the systems. Approximations for the pseudo-metrics can be obtained by considering Lyapunov-like functions called simulation and bisimulation functions. We illustrate our approximation framework in reducing the complexity of safety verification problems for both deterministic and nondeterministic continuous systems
15
Wojciech Penczek · Science of Computer Programming · 1990 · 4K citations
Symbolic model checking: 1020 States and beyond
Jerry R. Burch, E. M. Clarke, Kenneth L. McMillan et al. · Information and Computation · 1992 · 2.7K citations
Discrete abstractions of hybrid systems
Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere et al. · Proceedings of the IEEE · 2000 · 816 citations · Full text
Metrics for labelled Markov processes
Josée Desharnais, Vineet Gupta, Radha Jagadeesan et al. · Theoretical Computer Science · 2003 · 309 citations