{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T07:16:42Z","timestamp":1712301402901},"reference-count":24,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2017,8,23]],"date-time":"2017-08-23T00:00:00Z","timestamp":1503446400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2017,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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\u2014an 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<jats:sc>cplus2aspmt<\/jats:sc>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<jats:monospace>dReal<\/jats:monospace>.<\/jats:p>","DOI":"10.1017\/s1471068417000412","type":"journal-article","created":{"date-parts":[[2017,8,23]],"date-time":"2017-08-23T08:51:01Z","timestamp":1503478261000},"page":"924-941","source":"Crossref","is-referenced-by-count":1,"title":["Representing hybrid automata by action language modulo theories"],"prefix":"10.1017","volume":"17","author":[{"given":"JOOHYUNG","family":"LEE","sequence":"first","affiliation":[]},{"given":"NIKHIL","family":"LONEY","sequence":"additional","affiliation":[]},{"given":"YUNSONG","family":"MENG","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,8,23]]},"reference":[{"key":"S1471068417000412_ref14","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1613\/jair.2044","article-title":"Modelling mixed discrete-continuous domains for planning","volume":"27","author":"Fox","year":"2006","journal-title":"Journal of Artificial Intelligence Research (JAIR)"},{"key":"S1471068417000412_ref4","unstructured":"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)."},{"key":"S1471068417000412_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2002.12.001"},{"key":"S1471068417000412_ref10","unstructured":"Cimatti A. , Mover S. and Tonetta S. 2012. SMT-based verification of hybrid systems. In Proc. of AAAI, 2100\u20132105."},{"key":"S1471068417000412_ref12","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-150697"},{"key":"S1471068417000412_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9116-y"},{"key":"S1471068417000412_ref18","first-page":"195","article-title":"Action languages 7","volume":"3","author":"Gelfond","year":"1998","journal-title":"Electronic Transactions on Artificial Intelligence"},{"key":"S1471068417000412_ref6","unstructured":"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\u20133253."},{"key":"S1471068417000412_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30743-0_38"},{"key":"S1471068417000412_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20144-8"},{"key":"S1471068417000412_ref3","doi-asserted-by":"crossref","unstructured":"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\u2013134.","DOI":"10.1007\/978-3-642-40564-8_13"},{"key":"S1471068417000412_ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TCIAIG.2015.2509600"},{"key":"S1471068417000412_ref2","doi-asserted-by":"crossref","unstructured":"Alur R. , Henzinger T. A. , Lafferriere G. and Pappas G. J. 2000. Discrete abstractions of hybrid systems. In Proc. of the IEEE. 971\u2013984.","DOI":"10.1109\/5.871304"},{"key":"S1471068417000412_ref22","unstructured":"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\u2013996."},{"key":"S1471068417000412_ref8","unstructured":"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)."},{"key":"S1471068417000412_ref17","doi-asserted-by":"crossref","unstructured":"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\u2013364.","DOI":"10.1007\/978-3-642-15675-5_32"},{"key":"S1471068417000412_ref20","doi-asserted-by":"crossref","unstructured":"Henzinger T. A. 1996. The theory of hybrid automata. In Proc. of 11th Annual IEEE Symposium on Logic in Computer Science, 278\u2013292.","DOI":"10.1109\/LICS.1996.561342"},{"key":"S1471068417000412_ref15","unstructured":"Gao S. , Kong S. and Clarke E. 2013a. Satisfiability modulo ODEs. FMCAD, 105\u2013112."},{"key":"S1471068417000412_ref23","unstructured":"Lygeros J. 2004. Lecture notes on hybrid systems. University of Patras, Technical Report."},{"key":"S1471068417000412_ref1","doi-asserted-by":"crossref","unstructured":"Alur R. 2011. Formal verification of hybrid systems. In Proc. of the International Conference on Embedded Software (EMSOFT'11), IEEE, 273\u2013278.","DOI":"10.1145\/2038642.2038685"},{"key":"S1471068417000412_ref21","doi-asserted-by":"crossref","unstructured":"Lee J. , Loney N. and Meng Y. 2017. Online appendix for the paper \u201crepresenting hybrid automata by action language modulo theories\u201d. TPLP Archive.","DOI":"10.1017\/S1471068417000412"},{"key":"S1471068417000412_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.04.011"},{"key":"S1471068417000412_ref16","doi-asserted-by":"crossref","unstructured":"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\u2013214.","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"S1471068417000412_ref5","unstructured":"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\u2013724."}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068417000412","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T14:20:33Z","timestamp":1570026033000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068417000412\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,23]]},"references-count":24,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["S1471068417000412"],"URL":"https:\/\/doi.org\/10.1017\/s1471068417000412","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,23]]}}}