Representing hybrid automata by action language modulo theories

Joohyung Lee, Nikhil Loney, Yunsong Meng

Research output: Contribution to journalArticle

1 Citation (Scopus)

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 - 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 ordinary differential equations, which can be compiled into satisfiability modulo ordinary differential equations. We present 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.

Original languageEnglish (US)
Pages (from-to)924-941
Number of pages18
JournalTheory and Practice of Logic Programming
Volume17
Issue number5-6
DOIs
StatePublished - Sep 1 2017

Fingerprint

Hybrid Automata
Ordinary differential equations
Modulo
Programming theory
Dynamical systems
Ordinary differential equation
Answer Sets
Answer Set Programming
Invariant
Language
Transition Systems
Hybrid Systems
Notation
Dynamic Systems
Prototype
First-order
Computing

Keywords

  • Action languages
  • Answer set programming
  • Hybrid automata

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computational Theory and Mathematics
  • Artificial Intelligence

Cite this

Representing hybrid automata by action language modulo theories. / Lee, Joohyung; Loney, Nikhil; Meng, Yunsong.

In: Theory and Practice of Logic Programming, Vol. 17, No. 5-6, 01.09.2017, p. 924-941.

Research output: Contribution to journalArticle

Lee, Joohyung ; Loney, Nikhil ; Meng, Yunsong. / Representing hybrid automata by action language modulo theories. In: Theory and Practice of Logic Programming. 2017 ; Vol. 17, No. 5-6. pp. 924-941.
@article{e9a44e8ac59a4fe1bcf114c4a85ba7fe,
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 - 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 ordinary differential equations, which can be compiled into satisfiability modulo ordinary differential equations. We present 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.",
keywords = "Action languages, Answer set programming, Hybrid automata",
author = "Joohyung Lee and Nikhil Loney and Yunsong Meng",
year = "2017",
month = "9",
day = "1",
doi = "10.1017/S1471068417000412",
language = "English (US)",
volume = "17",
pages = "924--941",
journal = "Theory and Practice of Logic Programming",
issn = "1471-0684",
publisher = "Cambridge University Press",
number = "5-6",

}

TY - JOUR

T1 - Representing hybrid automata by action language modulo theories

AU - Lee, Joohyung

AU - Loney, Nikhil

AU - Meng, Yunsong

PY - 2017/9/1

Y1 - 2017/9/1

N2 - 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 - 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 ordinary differential equations, which can be compiled into satisfiability modulo ordinary differential equations. We present 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.

AB - 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 - 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 ordinary differential equations, which can be compiled into satisfiability modulo ordinary differential equations. We present 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.

KW - Action languages

KW - Answer set programming

KW - Hybrid automata

UR - http://www.scopus.com/inward/record.url?scp=85032583301&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85032583301&partnerID=8YFLogxK

U2 - 10.1017/S1471068417000412

DO - 10.1017/S1471068417000412

M3 - Article

AN - SCOPUS:85032583301

VL - 17

SP - 924

EP - 941

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

SN - 1471-0684

IS - 5-6

ER -