Show simple item record

dc.contributor.authorDing, Xuchuen_US
dc.contributor.authorLazar, Mirceaen_US
dc.contributor.authorBelta, Calinen_US
dc.date.accessioned2018-07-13T18:05:09Z
dc.date.available2018-07-13T18:05:09Z
dc.date.issued2012
dc.identifier.citationXuchu Ding, Mircea Lazar, Calin Belta. 2012. "Formal Abstraction of Linear Systems via Polyhedral Lyapunov Functions*." IFAC Proceedings Volumes, v. 45, issue 9, pp. 88 - 93.
dc.identifier.issn1474-6670
dc.identifier.urihttps://hdl.handle.net/2144/29852
dc.description.abstractIn this paper we present an abstraction algorithm that produces a finite bisimulation quotient for an autonomous discrete-time linear system. We assume that the bisimulation quotient is required to preserve the observations over an arbitrary, finite number of polytopic subsets of the system state space. We generate the bisimulation quotient with the aid of a sequence of contractive polytopic sublevel sets obtained via a polyhedral Lyapunov function. The proposed algorithm guarantees that at iteration i, the bisimulation of the system within the i-th sublevel set of the Lyapunov function is completed. We then show how to use the obtained bisimulation quotient to verify the system with respect to arbitrary Linear Temporal Logic formulas over the observed regions.en_US
dc.format.extentp. 88-93en_US
dc.relation.ispartofIFAC Proceedings Volumes
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 Internationalen_US
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/
dc.subjectSystems and controlen_US
dc.subjectOptimization and controlen_US
dc.titleFormal abstraction of linear systems via polyhedral Lyapunov functions*en_US
dc.typeArticleen_US
dc.identifier.doi10.3182/20120606-3-NL-3011.00096
pubs.elements-sourcecrossrefen_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

Attribution-NonCommercial-NoDerivatives 4.0 International
Except where otherwise noted, this item's license is described as Attribution-NonCommercial-NoDerivatives 4.0 International