AFSEC

Session AFSEC pendant les journées du GDR GPL

7th June 2021

Les journées du GDR GPL se tiendront du lundi 14 au vendredi 18 juin prochain, à distance. À cette occasion, une session AFSEC sera organisée le mercredi 16 juin de 13h30 à 15h30. Deux exposés sur la thématique des solveurs SMT seront donnés. Pour s’inscrire c’est ici : https://gdr-gpl-2021.sciencesconf.org/

On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets (par Nicolas Amat)

We define a method for taking advantage of net reductions in combination with a SMT-based model checker. We prove the correctness of this method using a new notion of equivalence between nets that we call polyhedral abstraction. Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used during the 2020 edition of the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions.

SMT-Based Bounded Model Checking of Max-Plus Linear Systems (par Muhammad Syifa’ul Mufid)

Max-Plus Linear (MPL) systems are an algebraic formalism with practical applications in transportation networks, manufacturing and biological systems. MPL systems can be naturally modeled as infinite-state transition systems, and exhibit interesting structural properties (e.g. periodicity or steady-state), for which analysis methods have been recently proposed. In this talk, we tackle the open problem of specifying and analyzing user-defined temporal properties for MPL systems. We propose Time-Difference LTL (TDLTL), a logic that encompasses the delays between the discrete-time events governed by an MPL system, and characterizes the problem of model checking TDLTL over MPL. We propose a family of specialized algorithms leveraging the periodic behaviour of an MPL system. We prove soundness and completeness, showing that the transient and cyclicity of the MPL system induce a completeness threshold for the verification problem. The algorithms are cast in the setting of SMT-based verification of infinite-state transition systems over the reals, with variants depending on the computation of the bound, and on the unrolling of the transition relation. Our comprehensive experiments show that the proposed techniques can be applied to MPL systems of large dimensions and on general TDLTL formulae, with remarkable performance gains against a dedicated abstraction-based technique and a translation to the nuXmv symbolic model checker.

Leave a Reply

You must be logged in to post a comment.