Diagnostic Information for Realizability
From MaRDI portal
Publication:5452707
DOI10.1007/978-3-540-78163-9_9zbMATH Open1138.68442DBLPconf/vmcai/CimattiRST08OpenAlexW1603488308WikidataQ62041285 ScholiaQ62041285MaRDI QIDQ5452707FDOQ5452707
Recommendations
Cites work
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 1487476 (Why is no real title available?)
- scientific article; zbMATH DE number 2102731 (Why is no real title available?)
- scientific article; zbMATH DE number 2112979 (Why is no real title available?)
- Boolean Abstraction for Temporal Logic Satisfiability
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- Counterexamples revisited: principles, algorithms, applications
- Diagnostic Information for Realizability
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification, Model Checking, and Abstract Interpretation
Cited in
(47)- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Control design for specifications on stochastic hybrid systems
- Iterative temporal motion planning for hybrid systems in partially unknown environments
- Flowpipe approximation and clustering in space-time
- Performance heuristics for GR(1) synthesis and related algorithms
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- Analysing sanity of requirements for avionics systems
- Observer design for a class of piecewise affine hybrid systems
- Tracking differentiable trajectories across polyhedra boundaries
- Limited-information control of hybrid systems via reachable set propagation
- Quantitative timed simulation functions and refinement metrics for real-time systems
- Detecting unrealizability of distributed fault-tolerant systems
- GR(1)*: GR(1) specifications extended with existential guarantees
- Diagnostic Information for Realizability
- Mining requirements from closed-loop control models
- Optimal CPU allocation to a set of control tasks with soft real-time execution constraints
- Stabhyli -- a tool for automatic stability verification of non-linear hybrid systems
- Zélus: a synchronous language with ODEs
- Generating diagnostic information for behavioral preorders
- On the decidability of stability of hybrid systems
- GR(1)*: GR(1) specifications extended with existential guarantees
- Safe schedulability of bounded-rate multi-mode systems
- Hybrid control Lyapunov functions for the stabilization of hybrid systems
- Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
- Shield synthesis
- Synthesis of Reactive(1) designs
- Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets
- Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
- Lyapunov analysis of rigid body systems with impacts and friction via sums-of-squares
- Least-violating control strategy synthesis with safety rules
- Pricing Diagnostic Information
- Automated analysis of real-time scheduling using graph games
- Bounded model-checking of discrete duration calculus
- Temporal logic model predictive control for discrete-time systems
- Compositional heterogeneous abstraction
- One-shot computation of reachable sets for differential games
- Resilient synchronization in robust networked multi-agent systems
- Rewarding probabilistic hybrid automata
- State estimation for polyhedral hybrid systems and applications to the Godunov scheme
- Extracting unsatisfiable cores for LTL via temporal resolution
- A toolbox for simulation of hybrid systems in Matlab/Simulink. Hybrid Equations (HyEQ) Toolbox
- Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems
- Specification-guided controller synthesis for linear systems and safe linear-time temporal logic
- Learning nonlinear hybrid systems: from sparse optimization to support vector regression
- A weakness measure for GR(1) formulae
- A weakness measure for GR(1) formulae
- Interpolation-based GR(1) assumptions refinement
This page was built for publication: Diagnostic Information for Realizability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5452707)
