Abstractions and formal verification of max-plus linear systems

Thesis

Max-Plus Linear (MPL) systems are the class of discrete-event systems (DES) with dynamics based on two binary operations (maximisation and addition) over the so-called max-plus semiring. In practical applications, MPL systems are used to model synchronisation phenomena without concurrency. Such are widely used in railway networks, manufacturing plants, and modelling and studying biological systems. The dual of MPL systems is Min-Plus Linear (MiPL) systems which use minimisation and additio...

Expand abstract

Authors: Syifaul Mufid, M

• DOI: 10.5287/ora-4jq4dg782
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: formal verification; abstractions; min-plus linear systems; Satisfiability Modulo Theory; interval max-plus linear systems; linear temporal logic; model checking and bounded model checking; difference logic; linear real arithmetic; max-plus linear systems
• Subjects: Formal methods (Computer science)