1 
Über abstrakte Charakterisierungen von BisimulationRoggenbach, Markus. Unknown Date (has links)
Universiẗat, Diss., 1998Mannheim.

2 
Contextdependent bisimulation between processesLarsen, Kim Guldstrand January 1986 (has links)
No description available.

3 
Bisimulationen und Äquivalenzbegriffe für Transitionssysteme und EreignisstrukturenChristgau, Martin. January 1995 (has links)
Mannheim, Univ., Diplomarbeit, 1995.

4 
Guarded logics: algorithms and bisimulationHirsch, Colin. Unknown Date (has links) (PDF)
Techn. Hochsch., Diss., 2002Aachen.

5 
Improving scalability of exploratory model checkingBoulgakov, Alexandre January 2016 (has links)
As software and hardware systems grow more complex and we begin to rely more on their correctness and reliability, it becomes exceedingly important to formally verify certain properties of these systems. If done naïvely, verifying a system can easily require exponentially more work than running it, in order to account for all possible executions. However, there are often symmetries or other properties of a system that can be exploited to reduce the amount of necessary work. In this thesis, we present a number of approaches that do this in the context of the CSP model checker FDR. CSP is named for Communicating Sequential Processes, or parallel combinations of state machines with synchronised communications. In the FDR model, the component processes are typically converted to explicit state machines while their parallel combination is evaluated lazily during model checking. Our contributions are motivated by this model but applicable to other models as well. We first address the scalability of the component machines by proposing a lazy compiler for a subset of CSP<sub>M</sub> selected to model parameterised state machines. This is a typical case where the state space explosion can make model checking impractical, since the size of the state space is exponential in the number and size of the parameters. A lazy approach to evaluating these systems allows only the reachable subset of the state space to be explored. As an example, in studying security protocols, it is common to model an intruder parameterised by knowledge of each of a list of facts; even a relatively small 100 facts results in an intractable 2<sup>100</sup> states, but the rest of the system can ensure that only a small number of these states are reachable. Next, we address the scalability of the overall combination by presenting novel algorithms for bisimulation reduction with respect to strong bisimulation, divergence respecting delay bisimulation, and divergencerespecting weak bisimulation. Since a parallel composition is related to the Cartesian product of its components, performing a relatively timeconsuming bisimulation reduction on the components can reduce its size significantly; an efficient bisimulation algorithm is therefore very desirable. This thesis is motivated by practical implementations, and we discuss an implementation of each of the proposed algorithms in FDR. We thoroughly evaluate their performance and demonstrate their effectiveness.

6 
Reduction Techniques for Finite (Tree) AutomataKaati, Lisa January 2008 (has links)
Finite automata appear in almost every branch of computer science, for example in model checking, in natural language processing and in database theory. In many applications where finite automata occur, it is highly desirable to deal with automata that are as small as possible, in order to save memory as well as excecution time. Deterministic finite automata (DFAs) can be minimized efficiently, i.e., a DFA can be converted to an equivalent DFA that has a minimal number of states. This is not the case for nondeterministic finite automata (NFAs). To minimize an NFA we need to compute the corresponding DFA using subset construction and minimize the resulting automaton. However, subset construction may lead to an exponential blowup in the size of the automaton and therefore even if the minimal DFA may be small, it might not be feasible to compute it in practice since we need to perform the expensive subset construction. To aviod subset construction we can reduce the size of an NFA using heuristic methods. This can be done by identifying and collapsing states that are equal with respect to some suitable equivalence relation that preserves the language of the automaton. The choice of an equivalence relation is a tradeoff between the desired amount of reduction and the computation time since the coarser a relation is, the more expensive it is to compute. This way we obtain a reduction method for NFAs that is useful in practice. In this thesis we address the problem of reducing the size of nondeterministic automata. We consider two different computation models: finite tree automata and finite automata. Finite automata can be seen as a special case of finite tree automata and all of the previously mentioned results concerning finite automata are applicable to tree automata as well. For nondeterministic bottomup tree automata, we present a broad spectrum of different relations that can be used to reduce their size. The relations differ in their computational complexity and reduction capabilities. We also provide efficient algorithms to compute the relations where we translate the problem of computing a given relation on a tree automaton to the problem of computing the relation on a finite automaton. For finite automata, we have extended and reformulated two algorithms for computing bisimulation and simulation on transition systems to operate on finite automata with alphabets. In particular, we consider a model of automata where the labels are encoded symbolically and we provide an algorithm for computing bisimulation on this partial symbolic encoding.

7 
A Tableau Algorithm for the Clique Guarded Fragment: Preliminary VersionHirsch, Colin, Tobies, Stephan 20 May 2022 (has links)
Aus der Einleitung:
„The Guarded Fragment of firstorder logic, introduced by Andréka, van Benthem, and Németi, has been a succesful attempt to transfer many good properties of modal, temporal, and description logics to a larger fragment of predicate logic. Among these are decidability, the finite modal property, invariance under an appropriate variant of bisimulation, and other nice modal theoretic properties. ...”

8 
Protecting Functional Programs From LowLevel AttackersLarmuseau, Adriaan January 2016 (has links)
Software systems are growing ever larger. Early software systems were singular units developed by small teams of programmers writing in the same programming language. Modern software systems, on the other hand, consist of numerous interoperating components written by different teams and in different programming languages. While this more modular and diversified approach to software development has enabled us to build ever larger and more complex software systems, it has, however, made it harder to ensure the reliability and security of software systems. In this thesis we study and remedy the security flaws that arise when attempting to resolve the difference in abstractions between components written in highlevel functional programming languages and components written in imperative lowlevel programming languages. Highlevel functional programming languages, treat computation as the evaluation of mathematical functions. Lowlevel imperative programming languages, on the contrary, provide programmers with features that enable them to directly interact with the underlying hardware. While these features help programmers write more efficient software, they also make it easy to write malware through techniques such as buffer overflows and return oriented programming. Concretely, we develop new runtime approaches for protecting components written in functional programming languages from malicious components written in lowlevel programming languages by making using of an emerging memory isolation mechanism.This memory isolation mechanism is called the Protected Module Architecture (PMA). Informally, PMA isolates the code and data that reside within a certain area of memory by restricting access to that area based on the location of the program counter. We develop these runtime protection techniques that make use of PMA for three important areas where components written in functional programming languages are threatened by malicious lowlevel components: foreign function interfaces, abstract machines and compilation. In everyone of these three areas, we formally prove that our runtime protection techniques are indeed secure. In addtion to that we also provide implementations of our ideas through a fully functional compiler and a wellperforming abstract machine.

9 
Reasoning About Multistage ProgramsInoue, Jun 24 July 2013 (has links)
Multistage programming (MSP) is a style of writing program
generatorsprograms which generate programssupported by special
annotations that direct construction, combination, and execution of
object programs. Various researchers have shown MSP to be effective
in writing efficient programs without sacrificing genericity.
However, correctness proofs of such programs have so far received
limited attention, and approaches and challenges for that task have
been largely unexplored. In this thesis, I establish formal
equational properties of the multistage lambda calculus and related
proof techniques, as well as results that delineate the intricacies
of multistage languages that one must be aware of.
In particular, I settle three basic questions that naturally arise
when verifying multistage functional programs. Firstly, can adding
staging MSP to a language compromise the interchangeability of terms
that held in the original language? Unfortunately it can, and more
care is needed to reason about terms with free variables. Secondly,
staging annotations, as the term ``annotations'' suggests, are often
thought to be orthogonal to the behavior of a program, but when is
this formally guaranteed to be the case? I give termination
conditions that characterize when this guarantee holds. Finally, do
multistage languages satisfy extensional facts, for example that
functions agreeing on all arguments are equivalent? I develop a
sound and complete notion of applicative bisimulation, which can
establish not only extensionality but, in principle, any other valid
program equivalence as well. These results improve our general
understanding of staging and enable us to prove the correctness of
complicated multistage programs.

10 
A formal fault model for component based models of embedded systemsFischer, Marco January 2006 (has links)
Zugl.: Chemnitz, Techn. Univ., Diss., 2006

Page generated in 0.1085 seconds