Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions

Muhammad Syifa’ul Mufid; Dieky Adzkiya; Alessandro Abate

doi:10.1007/978-3-030-29662-9_9

Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions

Muhammad Syifa’ul Mufid^*, Dieky Adzkiya, Alessandro Abate

^*Corresponding author for this work

Laboratory of Analysis, Algebra, and Mathematics for Education

University of Oxford

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

4 Citations (Scopus)

Abstract

This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications under consideration. We focus on verifying time-difference specifications, which encompass the relation between successive events in MPL systems. We implement a bounded model checking (BMC) procedure over a predicate abstraction of the given MPL system, to verify the satisfaction of time-difference specifications. Our predicate abstractions are experimentally shown to improve on existing MPL abstractions algorithms. Furthermore, with focus on the BMC algorithm, we can provide an explicit upper bound on the completeness threshold by means of the transient and the cyclicity of the underlying MPL system.

Original language	English
Title of host publication	Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings
Editors	Étienne André, Mariëlle Stoelinga, Mariëlle Stoelinga
Publisher	Springer
Pages	142-159
Number of pages	18
ISBN (Print)	9783030296612
DOIs	https://doi.org/10.1007/978-3-030-29662-9_9
Publication status	Published - 2019
Event	17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019 - Amsterdam, Netherlands Duration: 27 Aug 2019 → 29 Aug 2019

Publication series

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

Conference

Conference	17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019
Country/Territory	Netherlands
City	Amsterdam
Period	27/08/19 → 29/08/19

Access to Document

10.1007/978-3-030-29662-9_9

Cite this

Syifa’ul Mufid, M., Adzkiya, D., & Abate, A. (2019). Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions. In É. André, M. Stoelinga, & M. Stoelinga (Eds.), Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings (pp. 142-159). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11750 LNCS). Springer. https://doi.org/10.1007/978-3-030-29662-9_9

Syifa’ul Mufid, Muhammad ; Adzkiya, Dieky ; Abate, Alessandro. / Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions. Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings. editor / Étienne André ; Mariëlle Stoelinga ; Mariëlle Stoelinga. Springer, 2019. pp. 142-159 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3e61762375164a21920f81f4ad1718b5,

title = "Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions",

abstract = "This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications under consideration. We focus on verifying time-difference specifications, which encompass the relation between successive events in MPL systems. We implement a bounded model checking (BMC) procedure over a predicate abstraction of the given MPL system, to verify the satisfaction of time-difference specifications. Our predicate abstractions are experimentally shown to improve on existing MPL abstractions algorithms. Furthermore, with focus on the BMC algorithm, we can provide an explicit upper bound on the completeness threshold by means of the transient and the cyclicity of the underlying MPL system.",

author = "{Syifa{\textquoteright}ul Mufid}, Muhammad and Dieky Adzkiya and Alessandro Abate",

note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.; 17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019 ; Conference date: 27-08-2019 Through 29-08-2019",

year = "2019",

doi = "10.1007/978-3-030-29662-9_9",

language = "English",

isbn = "9783030296612",

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

publisher = "Springer",

pages = "142--159",

editor = "{\'E}tienne Andr{\'e} and Mari{\"e}lle Stoelinga and Mari{\"e}lle Stoelinga",

booktitle = "Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings",

address = "Germany",

}

Syifa’ul Mufid, M, Adzkiya, D & Abate, A 2019, Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions. in É André, M Stoelinga & M Stoelinga (eds), Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11750 LNCS, Springer, pp. 142-159, 17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019, Amsterdam, Netherlands, 27/08/19. https://doi.org/10.1007/978-3-030-29662-9_9

Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions. / Syifa’ul Mufid, Muhammad; Adzkiya, Dieky; Abate, Alessandro.
Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings. ed. / Étienne André; Mariëlle Stoelinga; Mariëlle Stoelinga. Springer, 2019. p. 142-159 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11750 LNCS).

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

TY - GEN

T1 - Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions

AU - Syifa’ul Mufid, Muhammad

AU - Adzkiya, Dieky

AU - Abate, Alessandro

PY - 2019

Y1 - 2019

N2 - This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications under consideration. We focus on verifying time-difference specifications, which encompass the relation between successive events in MPL systems. We implement a bounded model checking (BMC) procedure over a predicate abstraction of the given MPL system, to verify the satisfaction of time-difference specifications. Our predicate abstractions are experimentally shown to improve on existing MPL abstractions algorithms. Furthermore, with focus on the BMC algorithm, we can provide an explicit upper bound on the completeness threshold by means of the transient and the cyclicity of the underlying MPL system.

AB - This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications under consideration. We focus on verifying time-difference specifications, which encompass the relation between successive events in MPL systems. We implement a bounded model checking (BMC) procedure over a predicate abstraction of the given MPL system, to verify the satisfaction of time-difference specifications. Our predicate abstractions are experimentally shown to improve on existing MPL abstractions algorithms. Furthermore, with focus on the BMC algorithm, we can provide an explicit upper bound on the completeness threshold by means of the transient and the cyclicity of the underlying MPL system.

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

U2 - 10.1007/978-3-030-29662-9_9

DO - 10.1007/978-3-030-29662-9_9

M3 - Conference contribution

AN - SCOPUS:85077129134

SN - 9783030296612

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

SP - 142

EP - 159

BT - Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings

A2 - André, Étienne

A2 - Stoelinga, Mariëlle

PB - Springer

T2 - 17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019

Y2 - 27 August 2019 through 29 August 2019

ER -

Syifa’ul Mufid M, Adzkiya D, Abate A. Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions. In André É, Stoelinga M, Stoelinga M, editors, Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings. Springer. 2019. p. 142-159. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-29662-9_9

Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this