Author name cluster

Gerald Lüttgen

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers

2 author rows

LPAR Conference 2020 Conference Paper

Learning Data Structure Shapes from Memory Graphs

Jan H. Boockmann
Gerald Lüttgen

This paper presents a novel algorithm for automatically learning recursive shape pred- icates from memory graphs, so as to formally describe the pointer-based data structures contained in a program. These predicates are expressed in separation logic and can be used, e. g. , to construct efficient secure wrappers that validate the shape of data structures exchanged between trust boundaries at runtime. Our approach first decomposes memory graph(s) into sub-graphs, each of which exhibits a single data structure, and generates candidate shape predicates of increasing complexity, which are expressed as rule sets in Prolog. Under separation logic semantics, a meta-interpreter then performs a systematic search for a subset of rules that form a shape predicate that non-trivially and concisely captures the data structure. Our algorithm is implemented in the prototype tool ShaPE and evaluated on examples from the real-world and the literature. It is shown that our approach indeed learns concise predicates for many standard data structures and their implementation variations, and thus alleviates software engineers from what has been a time-consuming manual task.

Details

TCS Journal 2016 Journal Article

Nondeterministic Modal Interfaces

Ferenc Bujtor
Sascha Fendrich
Gerald Lüttgen
Walter Vogler

Interface theories are employed in the component-based design of concurrent systems. They often emerge as combinations of Interface Automata (IA) and Modal Transition Systems (MTS), e. g. , Nyman et al. 's IOMTS, Bauer et al. 's MIO, Raclet et al. 's MI or our MIA. In this paper, we generalise MI to nondeterministic interfaces, for which we properly resolve the longstanding conflict between unspecified inputs being allowed in IA but forbidden in MTS. With this solution we achieve, in contrast to related work, an associative parallel composition, a compositional preorder, a conjunction on interfaces with dissimilar alphabets supporting perspective-based specifications, and a quotienting operator for decomposing nondeterministic specifications in a single theory. In addition, we define a hiding and a restriction operator, complement conjunction with a disjunction operator and illustrate our interface theory by means of a simple example.

Details DOI

TCS Journal 2011 Journal Article

Safe reasoning with Logic LTS

Gerald Lüttgen
Walter Vogler

Previous work has introduced the setting of Logic Labelled Transition Systems, called Logic LTS or LLTS for short, together with a variant of ready simulation as its fully-abstract refinement preorder, which allows one to compose operational specifications using a CSP-style parallel operator and the propositional connectives conjunction and disjunction. In this article, we show how a temporal logic for specifying safety properties may be embedded into LLTS so that (a) the temporal operators are compositional for ready simulation; (b) ready simulation, when restricted to pairs of processes and formulas, coincides with the logic’s satisfaction relation; (c) ready simulation, when restricted to formulas, is entailment. The utility of this setting as a semantic foundation for mixed operational and temporal-logic specification languages is demonstrated by means of a simple example. We also adopt the concept of may- and must-transitions from modal transition systems for notational convenience, and investigate the relation between modal refinement on modal transition systems and ready simulation on LLTS.

Details DOI

I&C Journal 2010 Journal Article

Is observational congruence on μ -expressions axiomatisable in equational Horn logic?

Michael Mendler
Gerald Lüttgen

It is well known that bisimulation on μ -expressions cannot be finitely axiomatised in equational logic. Complete axiomatisations such as those of Milner and Bloom/Ésik necessarily involve implicational rules. However, both systems rely on features beyond pure equational Horn logic: either rules that are impure by involving non-equational side-conditions, or rules that are schematically infinitary like the congruence rule which is not Horn. It is an open question whether these complications cannot be avoided in the proof-theoretically and computationally clean and powerful setting of second-order equational Horn logic. This paper presents a positive and a negative result regarding the axiomatisability of observational congruence in equational Horn logic. Firstly, we show how Milner’s impure rule system can be reworked into a pure Horn axiomatisation that is complete for guarded processes. Secondly, we prove that for unguarded processes, both Milner’s unique fixed point rule and Bloom/Ésik’s GA rule are incomplete without the congruence rule, and neither system has a complete extension in rank-1 equational axioms. It remains open whether there are higher-rank equational axioms or other Horn rules which would render Milner’s or Bloom/Ésik’s axiomatisations complete.

Details DOI

I&C Journal 2010 Journal Article

Ready simulation for concurrency: It’s logical!

Gerald Lüttgen
Walter Vogler

This article provides new insight into the connection between the trace-based lower part of van Glabbeek’s linear-time, branching-time spectrum and its simulation-based upper part. We establish that ready simulation is fully abstract with respect to failure inclusion, when adding the conjunction operator that was proposed by the authors in [TCS 373 (1–2) 19–40] to the standard setting of labelled transition systems with (CSP-style) parallel composition. More precisely, we actually prove a stronger result by considering a coarser relation than failure inclusion, namely a preorder that relates processes with respect to inconsistencies that may arise under conjunctive composition. Ready simulation is also shown to satisfy standard logic properties. In addition, our semantic formalism proves itself robust when adding disjunction, external choice and hiding operators, and is thus suited for studying mixed operational and logic languages. Finally, the utility of our formalism is demonstrated by means of a small example that deals with specifying and reasoning about mode logics within aircraft control systems.

Details DOI

TCS Journal 2007 Journal Article

Conjunction on processes: Full abstraction via ready-tree semantics

Gerald Lüttgen
Walter Vogler

A key problem in mixing operational (e. g. process-algebraic) and declarative (e. g. logical) styles of specification is how to deal with inconsistencies arising when composing processes under conjunction. This article introduces a conjunction operator on labelled transition systems capturing the basic intuition of ‘a and b = false’, and considers a naive preorder that demands that an inconsistent specification can only be refined by an inconsistent implementation. The main body of the article is concerned with characterizing the largest precongruence contained in the naive preorder. This characterization will be based on what we call ready-tree semantics, which is a variant of path-based possible-worlds semantics. We prove that the induced ready-tree preorder is compositional and fully abstract, and that the conjunction operator indeed reflects conjunction. The article’s results provide a foundation for, and an important step towards a unified framework that allows one to freely mix operators from process algebras and linear-time temporal logics.

Details DOI

I&C Journal 2007 Journal Article

Priority and abstraction in process algebra

Rance Cleaveland
Gerald Lüttgen
V. Natarajan

More than 15 years ago, Cleaveland and Hennessy proposed an extension of the process algebra CCS in which some actions may take priority over others. The theory was equipped with a behavioral congruence based on strong bisimulation. This article gives a full account of the challenges in, and the solutions employed for, defining a semantic theory of observation congruence for this process algebra. A full-abstraction result is presented whose proof relies on a novel approach based on successive approximations for identifying the largest congruence contained in an intuitive but naïve equivalence. Prioritized observation congruence is also characterized equationally for the class of finite processes, while its utility for system verification is demonstrated by an illustrative example.

Details DOI

TCS Journal 2006 Journal Article

Bisimulation on speed: A unified approach

Gerald Lüttgen
Walter Vogler

Two process-algebraic approaches have been developed for comparing two bisimulation-equivalent processes with respect to speed: the one of Moller/Tofts equips actions with lower time bounds, while the other by Lüttgen/Vogler considers upper time bounds instead. This article sheds new light on both approaches by testifying to their close relationship. We introduce a general, intuitive concept of “faster-than”, which is formalised by a notion of amortised faster-than preorder. When closing this preorder under all contexts, exactly the two faster-than preorders investigated by Moller/Tofts and Lüttgen/Vogler arise. For processes incorporating both lower and upper time bounds we also show that the largest precongruence contained in the amortised faster-than preorder is not a proper preorder but a timed bisimulation. In the light of this result we systematically investigate under which circumstances the amortised faster-than preorder degrades to an equivalence.

Details DOI

I&C Journal 2004 Journal Article

Bisimulation on speed: worst-case efficiency

Gerald Lüttgen
Walter Vogler

This paper introduces a novel (bi)simulation-based faster-than preorder which relates asynchronous processes, where the relative speeds of system components are indeterminate, with respect to their worst-case timing behavior. The study is conducted for a conservative extension of the process algebra CCS, called TACS, which permits the specification of upper time bounds on action occurrences. TACS complements work in plain process algebras which compares asynchronous processes with respect to their functional reactive behavior only, and in timed process algebras which focus on analyzing synchronous processes. The most unusual contribution is in showing that the proposed faster-than preorder coincides with several other preorders, two of which consider the absolute times at which actions occur in system runs. The paper also develops the semantic theory of TACS by studying congruence properties, equational laws, and abstractions from internal actions. Two examples, one dealing with mail delivery and one relating two implementations of a simple storage system, testify to the practical utility of the new theory.

Details DOI

TCS Journal 1998 Journal Article

A process algebra with distributed priorities

Ranee Cleaveland
Gerald Lüttgen
V. Natarajan

This paper presents a process algebra for distributed systems in which some actions may take precedence over others. The algebra is distinguished by the design decision that it only allows actions to pre-empt others at the same “location” and therefore captures a notion of localized precedence. Using Park's and Milner's notion of strong bisimulation as a basis, we develop a behavioral congruence and axiomatize it for finite processes; we also derive an associated observational congruence and present logical characterizations of our behavioral relations. Simple examples highlight the utility of the theory.

Details DOI