Events at MetaForum MF 6.131

–

We are witnessing the increased availability of powerful quantum computing facilities as a service; also, there are promising prospects of applying quantum computing in fields such as material-and drug discovery, as well as scheduling, and optimisation. With these prospects comes an inherent challenge of quality assurance of complex quantum programs. Quantum programs and programming frameworks …continue reading

–

Bounded bypass is a desirable and therefore commonly considered property of mutual exclusion algorithms. However, its exact definition is not always clear, particularly when it is characterised as a liveness property. In this presentation I will show three definitions of bounded bypass: a very strict interpretation of the common definition, and two potential weakenings. I …continue reading

–

Context-Free-Language Ordered Binary Decision Diagrams form an alternative to Binary Decision Diagrams. CFLOBDDs aim to minimize the space required to encode Boolean functions by reusing repeated patterns. This way CFLOBDDs can be exponentially smaller than their BDD counterparts. In this thesis, we investigate the effectiveness of CFLOBDDs for model checking. To this end, we evaluate the space …continue reading

–

TSP;ac, the theory of sequential processes with sequencing, attributes, and conditions, was previously created as a simplification of TSP;ps, which exists for the sake of a process theoretic counterpart to the classical correspondence between pushdown automata and context-free grammars. This theory has a mechanism called sequential value passing, used to transfer data between sequential processes. …continue reading

–

The formal analysis and verification of parallelized algorithms on list decision diagrams implemented in the Sylvan library are presented. The algorithms are parallelized by the Lace parallelization framework. Key components of Sylvan are modelled using mCRL2, a tool for analyzing concurrent systems, focusing on verifying the functional correctness of algorithms. The analysis begins with an …continue reading

–

This thesis studies the ω-completeness of process theories for parallel processes without communication, extended with constants for successful and unsuccessful termination. We look into the ω-completeness of the theories BSP,  which is the theory BSP extended with operators for parallel  composition and left merge, as well as PA0, which is the theory PA extended with …continue reading

–

This thesis presents the light signal case study as part of the FormaSig project, which aims to use formal methods to support the development of EULYNX – a European initiative to standardise interfaces of signalling systems. EULYNX specifies its interfaces using SysML, which is a semi-formal modelling language. Previous research has developed a formalisation for …continue reading

–

In this talk, I will focus on a connection between stable-failures refinement and the ioco conformance relation. Both behavioural relations underlie methodologies that have gained traction in industry: stable-failures refinement is used in several commercial Model-Driven Engineering tool suites, whereas the ioco conformance relation is used in Model-Based Testing tools. Refinement-based Model-Driven Engineering approaches promise …continue reading

–

Efficient algorithms have been developed to model check LTL formulae on-the-fly, such as the well-known Nested Depth-First Search, which uses a depth-first search (DFS) strategy. However, in some settings, such as when considering distributed model checking on a cluster, or many-core model checking using a Graphics Processing Unit (GPU), Breadth-First Search (BFS) is a more …continue reading

–

In process mining, grammatical inference is used to extract information from large amounts of data. One problem in grammatical inference is exact DFA identification: finding a smallest DFA that accepts and rejects given words. Empirical experiments are used to compare new algorithms with the state of the art for exact DFA identification. To investigate to …continue reading