-A A +A

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

TitleBounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions
Publication TypeConference Paper
Year of Publication2019
AuthorsMufid MSyifa'ul, Adzkiya D, Abate A
Conference NameFormal Modeling and Analysis of Timed Systems
PublisherSpringer International Publishing
Conference LocationCham
ISBN Number978-3-030-29662-9

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.


Oxford Control and Verification (OXCAV) Group

C/O Department of Computer Science

Wolfson Building, Parks Rd, Oxford OX1 3QD

T: +44 (0) 18656 10767

Education - This is a contributing Drupal Theme
Design by WeebPal.