Show simple item record

dc.contributor.authorSvorenova, Mariaen_US
dc.contributor.authorKretinsky, Janen_US
dc.contributor.authorChmelik, Martinen_US
dc.contributor.authorChatterjee, Krishnenduen_US
dc.contributor.authorCerna, Ivanaen_US
dc.contributor.authorBelta, Calinen_US
dc.date.accessioned2018-06-29T17:36:17Z
dc.date.available2018-06-29T17:36:17Z
dc.date.issued2017-02-01
dc.identifierhttp://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000390637000014&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=6e74115fe3da270499c3d65c9b17d654
dc.identifier.citationMaria Svorenova, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cerna, Calin Belta. 2017. "Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games." NONLINEAR ANALYSIS-HYBRID SYSTEMS, v. 23, pp. 230 - 253 (24).
dc.identifier.issn1751-570X
dc.identifier.issn1878-7460
dc.identifier.urihttps://hdl.handle.net/2144/29731
dc.description.abstractWe consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study.en_US
dc.description.sponsorshipThis work was partially supported by Czech Science Foundation grant 15-17564S, People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement 291734, European Research Council (ERC) grant 267989 (QUAREM) and Start grant (279307: Graph Games), Austrian Science Fund (FWF) grants S11402-N23 (RiSE), P23499-N23 and S11407-N23 (RiSE), Czech Ministry of Education Youth and Sports grant LH11065, Czech Science Foundation Grant No.15-08772S, and National Science Foundation (NSF) grants CMMI-1400167 and CNS-1035588. (15-17564S - Czech Science Foundation; 15-08772S - Czech Science Foundation; 291734 - European Union; 267989 - European Research Council (ERC); 279307 - European Research Council (ERC); S11402-N23 - Austrian Science Fund (FWF); P23499-N23 - Austrian Science Fund (FWF); S11407-N23 - Austrian Science Fund (FWF); LH11065 - Czech Ministry of Education Youth and Sports; CMMI-1400167 - National Science Foundation (NSF); CNS-1035588 - National Science Foundation (NSF))en_US
dc.format.extentp. 230 - 253en_US
dc.languageEnglish
dc.publisherELSEVIER SCI LTDen_US
dc.relation.ispartofNONLINEAR ANALYSIS-HYBRID SYSTEMS
dc.subjectMathematicsen_US
dc.subjectControlen_US
dc.subjectLinear stochastic systemen_US
dc.subjectTemporal logicen_US
dc.subjectAbstraction refinementen_US
dc.subjectGamesen_US
dc.subjectScience & technologyen_US
dc.subjectPhysical sciencesen_US
dc.subjectAutomation & control systemsen_US
dc.subjectMathematics, applieden_US
dc.subjectNumerical and computational mathematicsen_US
dc.subjectVerificationen_US
dc.subjectIndustrial engineering & automationen_US
dc.titleTemporal logic control for stochastic linear systems using abstraction refinement of probabilistic gamesen_US
dc.typeArticleen_US
dc.identifier.doi10.1016/j.nahs.2016.04.006
pubs.elements-sourceweb-of-scienceen_US
pubs.notesEmbargo: Not knownen_US
pubs.organisational-groupBoston Universityen_US
pubs.organisational-groupBoston University, College of Engineeringen_US
pubs.organisational-groupBoston University, College of Engineering, Department of Mechanical Engineeringen_US
pubs.publication-statusPublisheden_US


This item appears in the following Collection(s)

Show simple item record