An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty

DOI10.1016/J.ARTINT.2015.03.002zbMath1343.68237DBLPjournals/ai/CimattiMR15OpenAlexW2057587325WikidataQ62041107 ScholiaQ62041107MaRDI QIDQ892228

Andrea Micheli, Marco Roveri, Alessandro Cimatti

Publication date: 18 November 2015

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.artint.2015.03.002

zbMATH Keywords

weak controllabilitysatisfiability modulo theorystrategy synthesistemporal problems

Mathematics Subject Classification ID

Reasoning under uncertainty in the context of artificial intelligence (68T37) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (1)

Quantifying controllability in temporal networks with uncertainty

Uses Software

• Unnamed Item
• Yices
• z3
• Chaff
• OpenSMT
• MathSAT5

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Maintaining knowledge about temporal intervals
• Dynamic controllability via timed game automata
• Efficient solution techniques for disjunctive temporal reasoning problems
• Temporal constraint networks
• Partial cylindrical algebraic decomposition for quantifier elimination
• A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra
• Simplexity of the cube
• Solving strong controllability of temporal problems with uncertainty using SMT
• Model-based Theory Combination
• Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
• Applying Linear Quantifier Elimination
• Strong Controllability of Disjunctive Temporal Problems with Uncertainty
• Efficient Term-ITE Conversion for Satisfiability Modulo Theories
• Simplification by Cooperating Decision Procedures
• Handling contingency in temporal constraint networks: from consistency to controllabilities
• The MathSAT5 SMT Solver
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• A machine program for theorem-proving
• Computer Aided Verification

This page was built for publication: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty