Solving Temporal Problems Using SMT: Weak Controllability

Authors

  • Alessandro Cimatti Fondazione Bruno Kessler
  • Andrea Micheli Fondazione Bruno Kessler
  • Marco Roveri Fondazione Bruno Kessler

DOI:

https://doi.org/10.1609/aaai.v26i1.8136

Keywords:

Constraints, Temporal Problems, Weak Controllability, Strategy Extraction

Abstract

Temporal problems with uncertainty are a well established formalism to model time constraints of a system interacting with an uncertain environment. Several works have addressed the definition and the solving of controllability problems, and three degrees of controllability have been proposed: weak, strong, and dynamic. In this work we focus on weak controllability: we address both the decision and the strategy extraction problems. Extracting a strategy means finding a function from assignments to uncontrollable time points to assignments to controllable time points that fulfills all the temporal constraints. We address the two problems in the satisfiability modulo theory framework. We provide a clean and complete formalization of the problems, and we propose novel techniques to extract strategies. We also provide experimental evidence of the scalability and efficiency of the proposed techniques.

Downloads

Published

2021-09-20

How to Cite

Cimatti, A., Micheli, A., & Roveri, M. (2021). Solving Temporal Problems Using SMT: Weak Controllability. Proceedings of the AAAI Conference on Artificial Intelligence, 26(1), 448-454. https://doi.org/10.1609/aaai.v26i1.8136

Issue

Section

Constraints, Satisfiability, and Search