Diagnostic Information for Realizability
From MaRDI portal
Publication:5452707
DOI10.1007/978-3-540-78163-9_9zbMath1138.68442OpenAlexW1603488308WikidataQ62041285 ScholiaQ62041285MaRDI QIDQ5452707
A. Tchaltsev, Alessandro Cimatti, Viktor Schuppan, Marco Roveri
Publication date: 4 April 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-78163-9_9
Related Items (43)
Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Analysing sanity of requirements for avionics systems ⋮ Stabhyli ⋮ Shield synthesis ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Synthesis of Reactive(1) designs ⋮ Least-violating control strategy synthesis with safety rules ⋮ Limited-information control of hybrid systems via reachable set propagation ⋮ Resilient synchronization in robust networked multi-agent systems ⋮ Learning nonlinear hybrid systems ⋮ Mining requirements from closed-loop control models ⋮ On the decidability of stability of hybrid systems ⋮ Lyapunov analysis of rigid body systems with impacts and friction via sums-of-squares ⋮ Hybrid control lyapunov functions for the stabilization of hybridsystems ⋮ A toolbox for simulation of hybrid systems in matlab/simulink ⋮ Zélus ⋮ State estimation for polyhedral hybrid systems and applications to the Godunov scheme ⋮ Observer design for a class of piecewise affine hybrid systems ⋮ Automated analysis of real-time scheduling using graph games ⋮ Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets ⋮ One-shot computation of reachable sets for differential games ⋮ Tracking differentiable trajectories across polyhedra boundaries ⋮ Flowpipe approximation and clustering in space-time ⋮ Bounded model-checking of discrete duration calculus ⋮ Optimal CPU allocation to a set of control tasks with soft real--time execution constraints ⋮ Safe schedulability of bounded-rate multi-mode systems ⋮ Compositional heterogeneous abstraction ⋮ Quantitative timed simulation functions and refinement metrics for real-time systems ⋮ Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems ⋮ Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems ⋮ Control design for specifications on stochastic hybrid systems ⋮ Rewarding probabilistic hybrid automata ⋮ Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata ⋮ Specification-guided controller synthesis for linear systems and safe linear-time temporal logic ⋮ Temporal logic model predictive control for discrete-time systems ⋮ Iterative temporal motion planning for hybrid systems in partially unknown environments ⋮ Interpolation-Based GR(1) Assumptions Refinement ⋮ GR(1)*: GR(1) specifications extended with existential guarantees ⋮ Diagnostic Information for Realizability ⋮ A weakness measure for GR(1) formulae ⋮ A weakness measure for GR(1) formulae ⋮ Performance heuristics for GR(1) synthesis and related algorithms ⋮ Reactive synthesis with maximum realizability of linear temporal logic specifications
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- Verification: Theory and Practice
- Tools and Algorithms for the Construction and Analysis of Systems
- Boolean Abstraction for Temporal Logic Satisfiability
- Diagnostic Information for Realizability
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Diagnostic Information for Realizability
