Engineering constraint solvers for automatic analysis of probabilistic hybrid automata

DOI10.1016/j.jlap.2010.07.003zbMath1205.68252MaRDI QIDQ710668

Martin Fränzle, Tino Teige, Andreas Eggers

Publication date: 22 October 2010

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2010.07.003

zbMATH Keywords

bounded model checking; arithmetic constraint solving; probabilistic hybrid automata; stochastic satisfiability

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Related Items

Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs, Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems, Verification and Control of Probabilistic Rectangular Hybrid Automata, Formal Modelling, Analysis and Verification of Hybrid Systems

Uses Software

• HySAT
• MathSAT
• ABsolver

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reachability analysis of stochastic hybrid systems: a biodiesel production system
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• Derived eigenvalues of symmetric matrices, with applications to distance geometry
• APPSSAT: Approximate probabilistic planning using stochastic satisfiability
• Games against nature
• Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
• Stochastic hybrid systems. Theory and safety critical applications.
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• Heterogeneous constraint solving
• Parallel SAT Solving in Bounded Model Checking
• Interval arithmetic
• Stochastic Hybrid Systems
• Solving SAT and SAT Modulo Theories
• Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems
• SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
• Predicative programming Part I
• Stochastic stability properties of jump linear systems
• Hybrid Systems: Computation and Control
• Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Verification, Model Checking, and Abstract Interpretation
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Stochastic Boolean satisfiability