kth.sePublications KTH
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal synthesis of stochastic systems via control barrier certificates
2021 (English)In: IEEE Transactions on Automatic Control, ISSN 0018-9286, E-ISSN 1558-2523, Vol. 66, no 7, p. 3097-3110, article id 9157966Article in journal (Refereed) Published
Abstract [en]

This article focuses on synthesizing control policies for discrete-time stochastic control systems together with a lower bound on the probability that the systems satisfy the complex temporal properties. The desired properties of the system are expressed as linear temporal logic specifications over finite traces. In particular, our approach decomposes the given specification into simpler reachability tasks based on its automata representation. We, then, propose the use of so-called control barrier certificate to solve those simpler reachability tasks along with computing the corresponding controllers and probability bounds. Finally, we combine those controllers to obtain a hybrid control policy solving the considered problem. Under some assumptions, we also provide two systematic approaches for uncountable and finite input sets to search for control barrier certificates. We demonstrate the effectiveness of the proposed approach on a room temperature control and lane keeping of a vehicle modeled as a four-dimensional single-track kinematic model. We compare our results with the discretization-based methods in the literature.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers Inc. , 2021. Vol. 66, no 7, p. 3097-3110, article id 9157966
Keywords [en]
Barrier certificates, Formal synthesis, Linear temporal logic (LTL), Stochastic systems, Control system synthesis, Probability, Stochastic control systems, Temporal logic, Concrete system, Control barriers, Curse of dimensionality, Discretizations, Linear temporal logic, Temporal property, Discrete time control systems
National Category
Control Engineering
Identifiers
URN: urn:nbn:se:kth:diva-303216DOI: 10.1109/TAC.2020.3013916ISI: 000668858300012Scopus ID: 2-s2.0-85099544677OAI: oai:DiVA.org:kth-303216DiVA, id: diva2:1602027
Note

QC 20211011

Available from: 2021-10-11 Created: 2021-10-11 Last updated: 2022-06-25Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus
In the same journal
IEEE Transactions on Automatic Control
Control Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 20 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf