Model Repair for Probabilistic Systems
From MaRDI portal
Publication:3000664
DOI10.1007/978-3-642-19835-9_30zbMath1316.68070OpenAlexW1574505635MaRDI QIDQ3000664
Radu Grosu, Scott A. Smolka, Ezio Bartocci, C. R. Ramakrishnan, Panagiotis Katsaros
Publication date: 19 May 2011
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-19835-9_30
Nonlinear programming (90C30) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items (53)
Synthesizing optimal bias in randomized self-stabilization ⋮ Stabhyli ⋮ Solving systems of bilinear equations for transition rate reconstruction ⋮ Fine-tuning the odds in Bayesian networks ⋮ Gradient-descent for randomized controllers under partial observability ⋮ The complexity of reachability in parametric Markov decision processes ⋮ Rate lifting for stochastic process algebra -- exploiting structural properties ⋮ Parameter-Independent Strategies for pMDPs via POMDPs ⋮ Incremental Verification of Parametric and Reconfigurable Markov Chains ⋮ Parameter synthesis in Markov models: a gentle survey ⋮ 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 ⋮ Are Parametric Markov Chains Monotonic? ⋮ Automation of fault-tolerant graceful degradation ⋮ On the Complexity of Reachability in Parametric Markov Decision Processes ⋮ Sequential Convex Programming for the Efficient Verification of Parametric MDPs ⋮ Counterexample-guided inductive synthesis for probabilistic systems ⋮ Deniable Functional Encryption ⋮ Inductive synthesis for probabilistic programs reaches new horizons ⋮ Two AGM-style characterizations of model repair ⋮ A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models ⋮ It Sometimes Works: A Lifting Algorithm for Repair of Stochastic Process Algebra Models ⋮ System design of stochastic models using robustness of temporal properties ⋮ Smoothed model checking for uncertain continuous-time Markov chains
Uses Software
Cites Work
- Parametric probabilistic transition systems for system design and analysis
- A logic for reasoning about time and reliability
- Enhancing model checking in verification by AI techniques
- Vacuity Checking in the Modal Mu-Calculus*
- Stochastic Model Checking
- Algorithm 852
- Theoretical Aspects of Computing - ICTAC 2004
- Computer Aided Verification
This page was built for publication: Model Repair for Probabilistic Systems
