Michel Reniers: Partial-Order Reduction for Supervisory Controller Synthesis
A key challenge in the synthesis and subsequent analysis of supervisory controllers is the impact of state-space explosion caused by concurrency. The main bottleneck is often the memory needed to store the composition of plant and requirement automata and the resulting supervisor. Partial-order reduction (POR) is a well-established technique that alleviates this issue in the …continue reading
Rick Erkens: Term Rewriting based on Set Automaton Matching
In a previous talk I presented an efficient pattern matching algorithm based on the notion of set automaton. This matching algorithm can be exploited to implement efficient term rewriting procedures. These procedures interleave pattern matching steps and rewriting steps, and thus smoothly integrate redex discovery and subterm replacement. In particular this method is suitable to …continue reading
Flip van Spaendonck: Extending the Cones and Foci method
Proving two processes equivalent modulo branching bisimulation can be quite difficult and laborious. The cones and foci method seeks to simplify proving equivalence by assuming that, in most implementations, internal actions progress towards a state in which only externally visible actions are possible. In this talk, we will discuss the original technique, its incompleteness, and …continue reading
Erik de Vink: On Spatial Logics and Spatial Bisimulation
Logics expressing spatial properties go back to Tarksi. Often their semantics is based on topological spaces. Cianza et al. propose to use instead so-called closure spaces as underlying mathematical structure, because closure spaces comprise topological spaces as well as standard Kripke frames. In this talk we exploit the fact that finite Kripke frames induce quasi-discrete …continue reading
Bas Luttik: Axiomatising Sequencing and Signals
I will discuss a process algebra with constants for the deadlocked and accepting processes, action prefixing, non-deterministic choice, sequencing, signals and conditions. As Jos Baeten already mentioned in his FSA colloquium talk of October 7, 2021, a process can be specified with a guarded recursive specification over this process algebra if, and only if, it …continue reading
Mark Bouwman: Compositional state space generation
In the FormaSig project we translate communicating SysML state machines to mCRL2. Selecting and executing a transition consists of several transitions in the mCRL2 model. These internal state machines can be considered unobservable and are renamed to tau. Since many of these internal transitions can be combined, the bisimulation quotient is orders of magnitude smaller …continue reading
Jeroen Keiren: Towards effective unfolding of structured parameters in mCRL2
Data types such as lists and structured sorts enable the creation of concise process models in mCRL2. However, static analysis tools such as constant elimination, parameter elimination and sum elimination only consider process parameters as a single unit in their analysis. Therefore, the added structure in process parameters negatively affects these static analysis techniques. Groote …continue reading
Ferry Timmers: ASD to mCRL2, translating and raking, a retrospective
The past year I’ve been working on finalizing a translation from ASD (a specification language for control systems used by the industry) to mCRL2. This was not a trivial task since I was left without a formal specification of ASD. What ensued was reverse-engineering and lots of testing with purposefully built models. In the end, …continue reading
Tom Franken: Parallel Sorting Under Assumptions.
The talk will explore parallel sorting with the following assumptions on the parallel processors: The processors can only save a constant amount of parameters. The processors need references to access other processors. Notably, I’ll take a look at sorting networks and the AKS network and at Richard Cole’s Parallel Merge Sort algorithm, to see whether …continue reading
Jan Martens: Lowerbounds for partition refinement algorithms that decide bisimilarity
Most of the algorithms that decide strong bisimilarity for LTSs can be classified as partition refinement algorithms. This includes the most efficient and well-known Paige-Tarjan algorithm. In recent work we establish an Omega((m+n) log n) lowerbound for the time complexity of these partition refinement algorithms, matching the time complexity of the Paige-Tarjan algorithm. However there …continue reading