Automatic verification of application-tailored OSEK kernels - Deifel, Hans-Peter; Göttlinger, Merlin; Milius, Stefan; Schröder, Lutz; Dietrich, Christian; Lohmann, Daniel (2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017, 2017)

Coalgebra encoding for efficient minimization - Deifel, Hans-Peter; Milius, Stefan; Wißmann, Thorsten (Leibniz International Proceedings in Informatics, LIPIcs, 2021)
Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.
CRIS-Team Scopus Importer:2021-10-01
Keywords: Coalgebra; Minimization; Partition refinement; Transition systems

Distributed Coalgebraic Partition Refinement - Birkmann, Fabian; Deifel, Hans-Peter; Milius, Stefan (TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT II, 2022)
CRIS-Team WoS Importer:2022-04-29

From generic partition refinement to weighted tree automata minimization - Wißmann, Thorsten; Deifel, Hans-Peter; Milius, Stefan; Schröder, Lutz (Formal Aspects of Computing, 2021)
Partition refinement is a method for minimizing automata and transition systems of various types. Recently, we have developed a partition refinement algorithm that is generic in the transition type of the given system and matches the run time of the best known algorithms for many concrete types of systems, e.g. deterministic automata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by modelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run time analysis of our algorithm to cover additional instances, notably weighted automata and, more generally, weighted tree automata. For weights in a cancellative monoid we match, and for non-cancellative monoids such as (the additive monoid of) the tropical semiring even substantially improve, the asymptotic run time of the best known algorithms. We have implemented our algorithm in a generic tool that is easily instantiated to concrete system types by implementing a simple refinement interface. Moreover, the algorithm and the tool are modular, and partition refiners for new types of systems are obtained easily by composing pre-implemented basic functors. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.
Created from Fastlane, WoS look-up

Generic Partition Refinement and Weighted Tree Automata - Deifel, Hans-Peter; Milius, Stefan; Schröder, Lutz; Wißmann, Thorsten (Formal Methods – The Next 30 Years, 2019)
Partition refinement is a method for minimizing automata and transition systems of various types. Recently, we have developed a partition refinement algorithm that is generic in the transition type of the given system and matches the run time of the best known algorithms for many concrete types of systems, e.g. deterministic automata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by modelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run time analysis of our algorithm to cover additional instances, notably weighted automata and, more generally, weighted tree automata. For weights in a cancellative monoid we match, and for non-cancellative monoids such as (the additive monoid of) the tropical semiring even substantially improve, the asymptotic run time of the best known algorithms. We have implemented our algorithm in a generic tool that is easily instantiated to concrete system types by implementing a simple refinement interface. Moreover, the algorithm and the tool are modular, and partition refiners for new types of systems are obtained easily by composing pre-implemented basic functors. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.

Permutation games for the weakly aconjunctive μ -calculus - Hausmann, Daniel; Schröder, Lutz; Deifel, Hans-Peter (24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018, 2018)

Unifying Metadata-Based Storage Reconstruction and Carving with LAYR - Schneider, Janine; Milius, Stefan; Deifel, Hans-Peter; Freiling, Felix (Forensic Science International: Digital Investigation, 2020)
Storage resources are usually organized in abstraction layers in computing systems where higher level storage (e.g. files or file systems) is constructed from lower level storage (e.g. disk volumes). Many forensic storage reconstruction techniques exist that gather data at lower layers and interpret this data to reconstruct higher layers. On the one hand, there are metadata-based reconstruction techniques that interpret metadata structures to precisely reconstruct upper layer content. On the other hand, there are pattern-based techniques (carving) that focus mainly on deleted files that cannot be reconstructed by other methods. Instances resembling the former approach are Carrier's The Sleuth Kit (TSK) as well as many commercial tools, while the latter approach is used by file carvers like Foremost and Scalpel. Based on a formalization of storage abstraction layers, we show that all these techniques can be unified within a modular reconstruction framework. We define composition operators that allow to precisely express complex reconstruction tasks that involve both metadata-based and pattern-based techniques and allow to combine their respective strengths seamlessly in forensic analysis. We present LAYR, an implementation of our approach and show that it can automatically and reliably combine different reconstruction approache
CRIS-Team WoS Importer:2020-11-27
Keywords: Digital forensics