Enhancing model checking in verification by AI techniques
From MaRDI portal
Publication:1606310
DOI10.1016/S0004-3702(99)00039-9zbMath0996.68104OpenAlexW2035668577WikidataQ59259734 ScholiaQ59259734MaRDI QIDQ1606310
Francesco Buccafurri, Georg Gottlob, Nicola Leone, Thomas Eiter
Publication date: 24 July 2002
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0004-3702(99)00039-9
Logic in artificial intelligence (68T27) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (44)
Stabhyli ⋮ Model measuring for discrete and hybrid systems ⋮ The Complexity of Linear-Time Temporal Logic Model Repair ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ A theory of change for prioritised resilient and evolvable software systems ⋮ Model and program repair via group actions ⋮ Revising system specifications in temporal logic ⋮ Finding and fixing faults ⋮ Abstract model repair for probabilistic systems ⋮ 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 ⋮ CTL update of Kripke models through protections ⋮ Model Repair for Probabilistic Systems ⋮ On ACTL formulas having linear counterexamples ⋮ Two AGM-style characterizations of model repair ⋮ Program repair without regret
This page was built for publication: Enhancing model checking in verification by AI techniques
