Show simple item record

dc.contributor.authorSandler, Andrei
dc.contributor.authorTveretina, Olga
dc.contributor.editorFiliot, Emmanuel
dc.contributor.editorJungers, Raphaël
dc.contributor.editorPotapov, Igor
dc.date.accessioned2020-03-26T01:01:51Z
dc.date.available2020-03-26T01:01:51Z
dc.date.issued2019-09-06
dc.identifier.citationSandler , A & Tveretina , O 2019 , Deciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifolds . in E Filiot , R Jungers & I Potapov (eds) , Reachability Problems - 13th International Conference, RP 2019, Proceedings . vol. 11674 , Lecture Notes in Computer Science , vol. 11674 , Springer Nature , pp. 178-192 . https://doi.org/10.1007/978-3-030-30806-3_14
dc.identifier.isbn9783030308056
dc.identifier.isbn9783030308063
dc.identifier.urihttp://hdl.handle.net/2299/22489
dc.description© 2019 Springer-Verlag. This is a post-peer-review, pre-copyedit version of a paper published in Reachability Problems: 13th International Conference, RP 2019, Brussels, Belgium, September 11–13, 2019, Proceedings. The final authenticated version is available online at: http://dx.doi.org/10.1007/978-3-030-30806-3_14
dc.description.abstractA hybrid automaton is a finite state machine combined with some k real-valued continuous variables, where k determines the number of the automaton dimensions. This formalism is widely used for modelling safety-critical systems, and verification tasks for such systems can often be expressed as the reachability problem for hybrid automata. Asarin, Mysore, Pnueli and Schneider defined classes of hybrid automata lying on the boundary between decidability and undecidability in their seminal paper ‘Low dimensional hybrid systems - decidable, undecidable, don’t know’ [9]. They proved that certain decidable classes become undecidable when given a little additional computational power, and showed that the reachability question remains unsolved for some 2-dimensional systems. Piecewise Constant Derivative Systems on 2-dimensional manifolds (or PCD2m) constitute a class of hybrid automata for which decidability of the reachability problem is unknown. In this paper we show that the reachability problem becomes decidable for PCD2m if we slightly limit their dynamics, and thus we partially answer the open question of Asarin, Mysore, Pnueli and Schneider posed in [9].en
dc.format.extent15
dc.format.extent388402
dc.language.isoeng
dc.publisherSpringer Nature
dc.relation.ispartofReachability Problems - 13th International Conference, RP 2019, Proceedings
dc.relation.ispartofseriesLecture Notes in Computer Science
dc.subjectHybrid Systems, reachability, decidability
dc.subjectDecidability
dc.subjectHybrid systems
dc.subjectReachability
dc.subjectComputer Science(all)
dc.subjectComputational Theory and Mathematics
dc.subjectTheoretical Computer Science
dc.titleDeciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifoldsen
dc.contributor.institutionSchool of Physics, Engineering & Computer Science
dc.contributor.institutionBiocomputation Research Group
dc.date.embargoedUntil2020-09-06
dc.identifier.urlhttp://www.scopus.com/inward/record.url?scp=85072867688&partnerID=8YFLogxK
rioxxterms.versionofrecord10.1007/978-3-030-30806-3_14
rioxxterms.typeOther
herts.preservation.rarelyaccessedtrue


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record