Event Category: Colloquium

–

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

–

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

–

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

–

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

–

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

–

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

–

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

–

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

–

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