A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems

Young Min Kwon; Eunhee Kim; Gul Agha

doi:10.1007/978-3-031-43835-6_5

A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems

Young Min Kwon, Eunhee Kim, Gul Agha

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Validating properties of nonlinear systems is difficult given the complexity of solving nonlinear dynamics equations. In this paper, we develop an LTL-based model checking technique to specify and validate properties of a nonlinear system. The technique can hide the difficulties in handling nonlinear difference equations, simplify the specification of properties of physical systems, and provide a high level abstraction to analyze and control nonlinear systems. We apply the proposed technique to controller synthesis problems: determining a design for a simple nonlinear control system, and finding an appropriate dosage to prescribe for drug administration.

Original language	English (US)
Title of host publication	Quantitative Evaluation of Systems - 20th International Conference, QEST 2023, Proceedings
Editors	Nils Jansen, Mirco Tribastone
Publisher	Springer
Pages	65-81
Number of pages	17
ISBN (Print)	9783031438349
DOIs	https://doi.org/10.1007/978-3-031-43835-6_5
State	Published - 2023
Externally published	Yes
Event	20th International Conference on Quantitative Evaluation of SysTems, QEST 2023 - Antwerp, Belgium Duration: Sep 20 2023 → Sep 22 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14287 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	20th International Conference on Quantitative Evaluation of SysTems, QEST 2023
Country/Territory	Belgium
City	Antwerp
Period	9/20/23 → 9/22/23

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-031-43835-6_5

Library availability

Discover UIUC Full Text

Cite this

Kwon, Y. M., Kim, E., & Agha, G. (2023). A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems. In N. Jansen, & M. Tribastone (Eds.), Quantitative Evaluation of Systems - 20th International Conference, QEST 2023, Proceedings (pp. 65-81). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14287 LNCS). Springer. https://doi.org/10.1007/978-3-031-43835-6_5

A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems. / Kwon, Young Min; Kim, Eunhee; Agha, Gul.
Quantitative Evaluation of Systems - 20th International Conference, QEST 2023, Proceedings. ed. / Nils Jansen; Mirco Tribastone. Springer, 2023. p. 65-81 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14287 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kwon, YM, Kim, E & Agha, G 2023, A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems. in N Jansen & M Tribastone (eds), Quantitative Evaluation of Systems - 20th International Conference, QEST 2023, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14287 LNCS, Springer, pp. 65-81, 20th International Conference on Quantitative Evaluation of SysTems, QEST 2023, Antwerp, Belgium, 9/20/23. https://doi.org/10.1007/978-3-031-43835-6_5

Kwon YM, Kim E, Agha G. A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems. In Jansen N, Tribastone M, editors, Quantitative Evaluation of Systems - 20th International Conference, QEST 2023, Proceedings. Springer. 2023. p. 65-81. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-43835-6_5

Kwon, Young Min ; Kim, Eunhee ; Agha, Gul. / A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems. Quantitative Evaluation of Systems - 20th International Conference, QEST 2023, Proceedings. editor / Nils Jansen ; Mirco Tribastone. Springer, 2023. pp. 65-81 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{13cd10ad1fab4c8884c9f9bd019f85f1,

title = "A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems",

abstract = "Validating properties of nonlinear systems is difficult given the complexity of solving nonlinear dynamics equations. In this paper, we develop an LTL-based model checking technique to specify and validate properties of a nonlinear system. The technique can hide the difficulties in handling nonlinear difference equations, simplify the specification of properties of physical systems, and provide a high level abstraction to analyze and control nonlinear systems. We apply the proposed technique to controller synthesis problems: determining a design for a simple nonlinear control system, and finding an appropriate dosage to prescribe for drug administration.",

author = "Kwon, {Young Min} and Eunhee Kim and Gul Agha",

note = "Y. Kwon—This work was supported by NRF of MSIT, Korea (2021R1F1A104859812) and by the MSIT, Korea, under the ICTCCP (IITP-2020-2011-1-00783) supervised by the IITP.; 20th International Conference on Quantitative Evaluation of SysTems, QEST 2023 ; Conference date: 20-09-2023 Through 22-09-2023",

year = "2023",

doi = "10.1007/978-3-031-43835-6_5",

language = "English (US)",

isbn = "9783031438349",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "65--81",

editor = "Nils Jansen and Mirco Tribastone",

booktitle = "Quantitative Evaluation of Systems - 20th International Conference, QEST 2023, Proceedings",

address = "Germany",

}

TY - GEN

T1 - A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems

AU - Kwon, Young Min

AU - Kim, Eunhee

AU - Agha, Gul

N1 - Y. Kwon—This work was supported by NRF of MSIT, Korea (2021R1F1A104859812) and by the MSIT, Korea, under the ICTCCP (IITP-2020-2011-1-00783) supervised by the IITP.

PY - 2023

Y1 - 2023

N2 - Validating properties of nonlinear systems is difficult given the complexity of solving nonlinear dynamics equations. In this paper, we develop an LTL-based model checking technique to specify and validate properties of a nonlinear system. The technique can hide the difficulties in handling nonlinear difference equations, simplify the specification of properties of physical systems, and provide a high level abstraction to analyze and control nonlinear systems. We apply the proposed technique to controller synthesis problems: determining a design for a simple nonlinear control system, and finding an appropriate dosage to prescribe for drug administration.

AB - Validating properties of nonlinear systems is difficult given the complexity of solving nonlinear dynamics equations. In this paper, we develop an LTL-based model checking technique to specify and validate properties of a nonlinear system. The technique can hide the difficulties in handling nonlinear difference equations, simplify the specification of properties of physical systems, and provide a high level abstraction to analyze and control nonlinear systems. We apply the proposed technique to controller synthesis problems: determining a design for a simple nonlinear control system, and finding an appropriate dosage to prescribe for drug administration.

UR - http://www.scopus.com/inward/record.url?scp=85174250970&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85174250970&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-43835-6_5

DO - 10.1007/978-3-031-43835-6_5

M3 - Conference contribution

AN - SCOPUS:85174250970

SN - 9783031438349

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 65

EP - 81

BT - Quantitative Evaluation of Systems - 20th International Conference, QEST 2023, Proceedings

A2 - Jansen, Nils

A2 - Tribastone, Mirco

PB - Springer

T2 - 20th International Conference on Quantitative Evaluation of SysTems, QEST 2023

Y2 - 20 September 2023 through 22 September 2023

ER -