Title: Representing Hybrid Automata by Action Language Modulo Theories,
Abstract: Both hybrid automata and action languages are formalisms for describing the
evolution of dynamic systems. This paper establishes a formal relationship
between them. We show how to succinctly represent hybrid automata in an action
language which in turn is defined as a high-level notation for answer set
programming modulo theories (ASPMT) --- an extension of answer set programs to
the first-order level similar to the way satisfiability modulo theories (SMT)
extends propositional satisfiability (SAT). We first show how to represent
linear hybrid automata with convex invariants by an action language modulo
theories. A further translation into SMT allows for computing them using SMT
solvers that support arithmetic over reals. Next, we extend the representation
to the general class of non-linear hybrid automata allowing even non-convex
invariants. We represent them by an action language modulo ODE (Ordinary
Differential Equations), which can be compiled into satisfiability modulo ODE.
We developed a prototype system cplus2aspmt based on these translations, which
allows for a succinct representation of hybrid transition systems that can be
computed effectively by the state-of-the-art SMT solver dReal.