This talk is a continuation of the talk I gave at the FSA colloquium of 4 November 2021, where I showed how a system that consists of a collection of synchronously communicating automata can be learned in a compositional fashion. However, this requires a priori knowledge of the alphabet of each component, making the approach …continue reading

Nested quantifiers, such as ∀ int x, int y; 0 ≤ x < 5 ∧ 0 ≤ y < 3 ⇒ a[5y+x]>0, pose challenges for verification tools based on SMT solvers. An SMT solver cannot simply determine a[13]>0 using the quantifier, since it has trouble finding the correct values for x and y, in this …continue reading

Willemse and Wesselink extended the PBES solvers in the mCRL2 toolset to support extracting evidence (witnesses and counterexamples) in the form a subsystems of a labelled transition system. This extension requires adding additional information to the PBES. Stramaglia has previously shown a two-step approach to solving a PBES with additional information: we first solve its …continue reading

The Prinses Marijke Sluizen in Tiel form a part of the Dutch waterways connecting the river Rhine with the Amsterdam-Rijn kanaal, allowing intense ship traffic while protecting the hinterland against flooding when water in the Rhine is high. We made a behavioural model of a controller of this sluice complex including failure of sensors and …continue reading

During the past five years, we’ve been developing yet another implementation of Binary Decision Diagrams (BDDs). What sets our implementation apart from others is its non-recursive algorithms. This allows it to efficiently compute on BDDs larger than the RAM of your machine – this potentially pushes the limits of symbolic model checking. In this talk, …continue reading

In the context of geometric representations of spatial objects, we explore a modelchecking approach based on polyhedra. To this end we introduce the notion of a polyhedral poset model as counterpart of a polyhedron model endowed with so-called simplicial bisimilarity. The latter equivalence captures the the spatial logic SLCS-eta, which has in particular a path …continue reading

Analyzing configurable systems using formal techniques, such as feature causality [1], allows for further insights towards why certain configurations exhibit a particular effect. Typically, the valid configuration space is exponential with respect to the number of features, and thus optimizations on feature cause computation would be beneficial. In the previous talk, we have discussed some …continue reading

Knowledge compilation refers to translating a data structure into another one to enable better algorithmic properties for specific tasks. For instance, model counting (#SAT) and uniform random sampling are likely to be not efficiently solvable for formulas in conjunctive normal form (CNF). However, compiling a CNF into deterministic decompositional negation normal form (d-DNNF) enables an …continue reading

Fault trees are a widely used formalism for modeling failures in safety-critical systems and analyzing their reliability. Traditionally, fault trees are constructed manually by experts, which can be time-consuming and error-prone. In this line of research, we aim to automatically derive fault trees from inspection and monitoring data. Given data containing failures of individual components …continue reading

GPUexplore, a GPU-accelerated explicit-state LTL model checker, achieves significant speedups compared to sequential and multi-core CPU model checkers, but it is limited by the amount of memory available on GPUs. Partial-Order Reduction is a way to remedy this problem, by excluding unnecessary transitions and states from exploration. For this work, we implemented the ample and …continue reading