Hostname: page-component-7b7567c8c-tnzcf Total loading time: 0 Render date: 2026-11-15T08:43:00.736Z Has data issue: false hasContentIssue false
  • English
  • Français

Representing hybrid automata by action language modulo theories*

Published online by Cambridge University Press:  23 August 2017

JOOHYUNG LEE,
NIKHIL LONEY and
YUNSONG MENG
JOOHYUNG LEE
Affiliation:
School of Computing, Informatics and Decision Systems Engineering, Arizona State University, Tempe, AZ, USA (e-mail: joolee@asu.edu, nloney@asu.edu)
NIKHIL LONEY
Affiliation:
School of Computing, Informatics and Decision Systems Engineering, Arizona State University, Tempe, AZ, USA (e-mail: joolee@asu.edu, nloney@asu.edu)
YUNSONG MENG
Affiliation:
Houzz, Inc., Palo Alto, CA, USA (e-mail: Yunsong.Meng@asu.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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

Answer set programmingAction languagesHybrid automata

Information

Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 17 , Special Issue 5-6: 33rd International Conference on Logic Programming , September 2017, pp. 924 - 941
Copyright
Copyright © Cambridge University Press 2017 

Footnotes

*

This work was partially supported by the National Science Foundation under Grants IIS-1319794 and IIS-1526301.

References

Alur, R. 2011. Formal verification of hybrid systems. In Proc. of the International Conference on Embedded Software (EMSOFT'11), IEEE, 273–278.Google Scholar
Alur, R., Henzinger, T. A., Lafferriere, G. and Pappas, G. J. 2000. Discrete abstractions of hybrid systems. In Proc. of the IEEE. 971–984.Google Scholar
Babb, J. and Lee, J. 2013. Cplus2ASP: Computing action language + in answer set programming. In Proc. of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 122–134.Google Scholar
Balduccini, M., Magazzeni, D. and Maratea, M. 2016. PDDL+ planning via constraint answer set programming. In Proc. of the Working Notes of the 7th Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP).Google Scholar
Bartholomew, M. and Lee, J. 2013. Functional stable model semantics and answer set programming modulo theories. In Proc. of International Joint Conference on Artificial Intelligence (IJCAI), 718–724.Google Scholar
Bryce, D., Gao, S., Musliner, D. and Goldman, R. 2015. SMT-based nonlinear PDDL+ planning. In Proc. of the 29th AAAI Conference on Artificial Intelligence, 3247–3253.Google Scholar
Calimeri, F., Fink, M., Germano, S., Humenberger, A., Ianni, G., Redl, C., Stepanova, D., Tucci, A. and Wimmer, A. 2016. Angry-HEX: An artificial player for angry birds based on declarative knowledge bases. IEEE Transactions on Computational Intelligence and AI in Games 8, 2, 128–139.Google Scholar
Chintabathina, S., Gelfond, M. and Watson, R. 2005. Modeling hybrid domains using process description language 6 . In Proc. of Workshop on Answer Set Programming: Advances in Theory and Implementation (ASP'05).Google Scholar
Chintabathina, S. and Watson, R. 2012. A new incarnation of action language . In Correct Reasoning, Erdem, E., Lee, J., Lierler, Y., and Pearce, D., Eds. Lecture Notes in Computer Science, vol. 7265. Springer, 560–575.CrossRefGoogle Scholar
Cimatti, A., Mover, S. and Tonetta, S. 2012. SMT-based verification of hybrid systems. In Proc. of AAAI, 2100–2105.Google Scholar
Corke, P. 2011. Robotics, Vision and Control: Fundamental Algorithms in MATLAB, Vol. 73. Springer.Google Scholar
Erdem, E., Patoglu, V. and Schüller, P. 2016. A systematic analysis of levels of integration between high-level task planning and low-level feasibility checks. AI Communications 29, 2, 319–349.Google Scholar
Ferraris, P., Lee, J. and Lifschitz, V. 2011. Stable models and circumscription. Artificial Intelligence 175, 236–263.Google Scholar
Fox, M. and Long, D. 2006. Modelling mixed discrete-continuous domains for planning. Journal of Artificial Intelligence Research (JAIR) 27, 235–297.CrossRefGoogle Scholar
Gao, S., Kong, S. and Clarke, E. 2013a. Satisfiability modulo ODEs. FMCAD, 105–112.Google Scholar
Gao, S., Kong, S. and Clarke, E. M. 2013b. dReal: An SMT solver for nonlinear theories over the reals. In Proc. of International Conference on Automated Deduction. Springer, Berlin, Heidelberg, 208–214.Google Scholar
Gebser, M., Grote, T. and Schaub, T. 2010. Coala: A compiler from action languages to ASP. In Proc. of European Conference on Logics in Artificial Intelligence (JELIA), 360–364.Google Scholar
Gelfond, M. and Lifschitz, V. 1998. Action languages 7 . Electronic Transactions on Artificial Intelligence 3, 195–210.Google Scholar
Giunchiglia, E., Lee, J., Lifschitz, V., McCain, N. and Turner, H. 2004. Nonmonotonic causal theories. Artificial Intelligence 153, (1–2), 49–104.Google Scholar
Henzinger, T. A. 1996. The theory of hybrid automata. In Proc. of 11th Annual IEEE Symposium on Logic in Computer Science, 278–292.Google Scholar
Lee, J., Loney, N. and Meng, Y. 2017. Online appendix for the paper “representing hybrid automata by action language modulo theories”. TPLP Archive.CrossRefGoogle Scholar
Lee, J. and Meng, Y. 2013. Answer set programming modulo theories and reasoning about continuous changes. In Proc. of International Joint Conference on Artificial Intelligence (IJCAI), 990–996.Google Scholar
Lygeros, J. 2004. Lecture notes on hybrid systems. University of Patras, Technical Report.Google Scholar
Mellarkod, V. S., Gelfond, M. and Zhang, Y. 2008. Integrating answer set programming and constraint logic programming. Annals of Mathematics and Artificial Intelligence 53, 1–4, 251–287.Google Scholar
Supplementary material: PDF

Lee et al supplementary material

Online Appendix

Download Lee et al supplementary material(PDF)
PDF 470.3 KB