Diagnostic Information for Realizability
From MaRDI portal
Publication:5452707
DOI10.1007/978-3-540-78163-9_9zbMATH Open1138.68442DBLPconf/vmcai/CimattiRST08OpenAlexW1603488308WikidataQ62041285 ScholiaQ62041285MaRDI QIDQ5452707FDOQ5452707
Authors: Alessandro Cimatti, Marco Roveri, Viktor Schuppan, A. Tchaltsev
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
Recommendations
Cites Work
- Boolean Abstraction for Temporal Logic Satisfiability
- Diagnostic Information for Realizability
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- Title not available (Why is that?)
- Counterexamples revisited: principles, algorithms, applications
- Verification, Model Checking, and Abstract Interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
- Title not available (Why is that?)
Cited In (45)
- Flowpipe approximation and clustering in space-time
- Observer design for a class of piecewise affine hybrid systems
- Tracking differentiable trajectories across polyhedra boundaries
- GR(1)*: GR(1) specifications extended with existential guarantees
- Pricing Diagnostic Information
- Limited-information control of hybrid systems via reachable set propagation
- GR(1)*: GR(1) specifications extended with existential guarantees
- Extracting unsatisfiable cores for LTL via temporal resolution
- Performance heuristics for GR(1) synthesis and related algorithms
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- Diagnostic Information for Realizability
- Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
- Lyapunov analysis of rigid body systems with impacts and friction via sums-of-squares
- Automated analysis of real-time scheduling using graph games
- Safe schedulability of bounded-rate multi-mode systems
- Analysing sanity of requirements for avionics systems
- Shield synthesis
- Learning nonlinear hybrid systems
- Interpolation-Based GR(1) Assumptions Refinement
- Control design for specifications on stochastic hybrid systems
- Iterative temporal motion planning for hybrid systems in partially unknown environments
- Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
- Synthesis of Reactive(1) designs
- 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
- On the decidability of stability of hybrid systems
- Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets
- Stabhyli
- Optimal CPU allocation to a set of control tasks with soft real--time execution constraints
- A weakness measure for GR(1) formulae
- A weakness measure for GR(1) formulae
- 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
- Hybrid control lyapunov functions for the stabilization of hybridsystems
- Bounded model-checking of discrete duration calculus
- A toolbox for simulation of hybrid systems in matlab/simulink
- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Zélus
- Mining requirements from closed-loop control models
- Temporal logic model predictive control for discrete-time systems
- Quantitative timed simulation functions and refinement metrics for real-time systems
- Least-violating control strategy synthesis with safety rules
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)