Author name cluster

Walter Vogler

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.

24 papers

2 author rows

TCS Journal 2017 Journal Article

ACTL for Modal Interface Automata

Ferenc Bujtor
Walter Vogler

In previous work, we developed Modal Interface Automata (MIA), an interface theory combining the input/output behaviour of de Alfaro and Henzinger's Interface Automata with the modalities of Larsen's Modal Transition Systems and featuring a conjunction on MIAs. In this paper, we add a temporal logics to MIA based on De Nicola's ACTL. We show how to translate the logical operators to operators on MIAs such that a MIA satisfies a temporal formula if and only if it refines the translation of the formula. This way, MIAs allow heterogeneous specifications with a variety of operational and logical connectives.

Details DOI

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 2015 Journal Article

Error-pruning in interface automata

Ferenc Bujtor
Walter Vogler

De Alfaro and Henzinger introduced interface automata to model and study behavioural types. These come with alternating simulation as refinement and with a specific parallel composition: if one component receives an unexpected input, this is regarded as an error and the resp. error states are removed with a special pruning operation. In this paper, we return to the foundations of interface automata and study how refinement and parallel composition should be defined best. We take as basic requirement that an implementation must be error-free, if the specification is. For three variants of error-free, we consider the coarsest precongruence for parallel composition respecting the basic requirement. We find that pruning proves to be relevant in all cases and point out an important subtlety for systems that are not input-deterministic.

Details DOI

TCS Journal 2014 Journal Article

Recent advances in unfolding technique

Blai Bonet
Patrik Haslum
Victor Khomenko
Sylvie Thiébaux
Walter Vogler

We propose a new, and to date the most general, framework for Petri net unfolding, which broadens its applicability, makes it easier to use, and increases its efficiency. In particular: (i) we propose a user-oriented view of the unfolding technique, which simply tells which information will be preserved in the final prefix and how to declare an event a cut-off in the algorithm, while hiding the technical parameters like the adequate order; (ii) the notion of the adequate order is generalised to a well-founded relation, and the requirement that it must refine ⊂ is replaced by a weaker one; and (iii) the order in which the unfolding algorithm selects the possible extensions of the prefix is entirely disentangled from the cut-off condition. We demonstrate the usefulness of the developed theory on some case studies.

Details DOI

GandALF Workshop 2011 Workshop Paper

Automated Analysis of MUTEX Algorithms with FASE

Federico Buti
Massimo Callisto De Donato
Flavio Corradini
Maria Rita Di Berardini
Walter Vogler

In this paper we study the liveness of several MUTEX solutions by representing them as processes in PAFAS s, a CCS-like process algebra with a specific operator for modelling non-blocking reading behaviours. Verification is carried out using the tool FASE, exploiting a correspondence between violations of the liveness property and a special kind of cycles (called catastrophic cycles) in some transition system. We also compare our approach with others in the literature. The aim of this paper is twofold: on the one hand, we want to demonstrate the applicability of FASE to some concrete, meaningful examples; on the other hand, we want to study the impact of introducing non-blocking behaviours in modelling concurrent systems.

PDF 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

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

Component refinement and CSC-solving for STG decomposition

Mark Schaefer
Walter Vogler

STGs (Signal Transition Graphs) give a formalism for the description of asynchronous circuits based on Petri nets. To overcome the state explosion problem one may encounter during circuit synthesis, a nondeterministic algorithm for decomposing STGs was suggested by Chu and improved by one of the present authors. Here we study how CSC-solving–which is essential for circuit synthesis–can be combined with decomposition. For this purpose, the correctness definition for decomposition is enhanced with internal signals and hierarchical decomposition is proven correct. Based on this, it is shown that speed-independent CSC-solving preserves correctness and can be combined with decomposition. Furthermore, we use our new correctness definition to give the first correctness proof for the decomposition method of Carmona and Cortadella. Finally, we compare three different implementation relations for STGs: one derived from our correctness definition; one defined by Dill based on trace structures; and one derived from I/O-compatibility defined by Carmona and Cortadella.

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

Fair testing

Arend Rensink
Walter Vogler

In this paper we present a solution to the long-standing problem of characterising the coarsest liveness-preserving pre-congruence with respect to a full (TCSP-inspired) process algebra. In fact, we present two distinct characterisations, which give rise to the same relation: an operational one based on a De Nicola–Hennessy-like testing modality which we call should-testing, and a denotational one based on a refined notion of failures. One of the distinguishing characteristics of the should-testing pre-congruence is that it abstracts from divergences in the same way as Milner’s observation congruence, and as a consequence is strictly coarser than observation congruence. In other words, should-testing has a built-in fairness assumption. This is in itself a property long sought-after; it is in notable contrast to the well-known must-testing of De Nicola and Hennessy (denotationally characterised by a combination of failures and divergences), which treats divergence as catastrophic and hence is incompatible with observation congruence. Due to these characteristics, should-testing supports modular reasoning and allows to use the proof techniques of observation congruence, but also supports additional laws and techniques. Moreover, we show decidability of should-testing (on the basis of the denotational characterisation). Finally, we demonstrate its advantages by the application to a number of examples, including a scheduling problem, a version of the Alternating Bit-protocol, and fair lossy communication channels.

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

I&C Journal 2003 Journal Article

Faster asynchronous systems

Walter Vogler

A testing scenario in the sense of De Nicola and Hennessy is developed to measure the worst-case efficiency of asynchronous systems. The resulting testing-preorder is characterized with a variant of refusal traces and shown to satisfy some properties that make it attractive as a faster-than relation. Finally, one implementation of a bounded buffer is shown to be strictly faster than two others – in contrast to a result obtained with a different approach by Arun-Kumar and Hennessy.

Details DOI

TCS Journal 2002 Journal Article

Efficiency of asynchronous systems, read arcs, and the MUTEX-problem

Walter Vogler

Two solutions to the MUTEX-problem are compared w. r. t. their temporal efficiency. For this, a formerly developed efficiency testing for asynchronous systems is adapted to Petri nets with so-called read arcs. Furthermore, a compositional semantics for fair behaviour (in the sense of the progress assumption) is presented. On the one hand, this semantics is related to efficiency testing. On the other hand, it is used to specify formally what a solution to the MUTEX-problem is. It is shown that one of our solutions indeed satisfies this specification and that ordinary nets without read arcs cannot solve the MUTEX-problem.

Details DOI

TCS Journal 2002 Journal Article

Partial order semantics and read arcs

Walter Vogler

We study a new partial order semantics of Petri nets with read arcs, where read arcs model reading without consuming, which is often more adequate than the destructive-read-and-rewrite modelled in ordinary nets without read arcs. As basic observations we take ST-traces, which are sequences of transition starts and ends. We define processes of our nets and derive two partial orders modelling causality and start precedence. These partial orders are related to basic observations and their system states just as in the ordinary approach the single partial order of a process is related to firing sequences and reachable markings. Our approach also supports a new view of concurrency as captured by steps.

Details DOI

TCS Journal 2001 Journal Article

Fast asynchronous systems in dense time

Lars Jenner
Walter Vogler

A testing scenario in the sense of De Nicola and Hennessy is developed to measure the worst-case efficiency of asynchronous systems using dense time. For all three variants considered, it is shown that one can equivalently use discrete time; in the discrete versions, one variant coincides with an approach based on discrete time in Vogler (CONCUR95, Lecture Notes in Computer Science, vol. 962, Springer, Berlin, 1995, pp. 299–312), and thus we can clarify the assumptions behind this approach. The resulting testing-preorders are characterized with some kind of refusal traces and shown to satisfy some properties that make them attractive as faster-than relations. The three testing preorders are incomparable in general, but for some interesting classes of systems implications are shown.

Details DOI

MFCS Conference 1997 Conference Paper

Partial Order Semantics and Read Arcs

Walter Vogler

Abstract We study a new partial order semantics of Petri nets with read arcs, where read arcs model reading without consuming, which is often more adequate than the destructive-read-and-rewrite modelled in ordinary nets. As basic observations we take ST-traces, which are sequences of transition starts and ends. We define processes of our nets and derive two partial orders modelling causality and start precedence. These partial orders are related to observations and systems states as in the ordinary approach the single partial order of a process is related to firing sequences and reachable markings. Our approach also supports a new view of concurrency as captured by steps.

Details

I&C Journal 1996 Journal Article

The Limit of Splitn-Language Equivalence

Walter Vogler

Splitting is a simple form of action refinement that may be used to express the duration of actions. In particular, split n subdivides each action into n phases. Petri nets N and N ′ are split n -language equivalent if split n ( N ) and split n ( N ′) are language equivalent. It is known that these equivalences get finer and finer with increasing n. This paper characterizes the limit of this sequence by a newly defined partial order semantics. This semantics is obtained from the interval-semiword semantics, which is fully abstract for action refinement and language equivalence, by closing it under a special swap operation. The new swap equivalence lies strictly between interval-semiword and step-sequence equivalence.

Details DOI

TCS Journal 1993 Journal Article

Bisimulation and action refinement

Walter Vogler

For event structures with silent moves, we consider several types of bisimulation that incorporate “true” concurrency to a varying degree, and show how each can be lifted in a uniform way to a congruence with respect to action refinement. We prove that we have constructed the coarsest congruences that respect interleaving, pomset and history-preserving bisimulation.

Details DOI

TCS Journal 1991 Journal Article

Decidable boundedness problems for sets of graphs generated by hyperedge-replacement

Annegret Habel
Hans-Jörg Kreowski
Walter Vogler

Consider a class C of hyperedge-replacement graph grammars and a numeric function on graphs like the number of edges, the degree (i. e. , the maximum of the degrees of all nodes of a graph), the number of simple paths, the size of a maximum set of independent nodes, etc. Each such function induces a boundedness problem for the class C: Given a grammar HRG in C, are the function values of all graphs in the language L(HRG), generated by HRG, bounded by an integer or not? We show that the boundedness problem is decidable if the corresponding function is compatible with the derivation process of the grammars in C and if it is composed of maxima, sums, and products in a certain way. This decidability result applies particularly to the examples listed above. Various significant sets of graphs such as the set of series-parallel graphs, the set of (maximum) outerplanar graphs, the set of k-trees, and the set of graphs of cyclic bandwidth ⩽k can be generated by hyperedge-replacement graph grammars. Hence, the study in this paper is not only attributed to the area of graph grammars but may also interest those who investigate graph-theoretic properties of particular sets of graphs.

Details DOI

TCS Journal 1991 Journal Article

Executions: a new partial-order semantics of Petri nets

Walter Vogler

Executions, a new partial-order semantics of P/T nets, are defined as a generalization of the processes of safe nets. Various relations between executions and processes are established; especially, it is shown that for each net N there is a safe net SN(N) such that the processes of SN(N) are isomorphic to the executions of N. Furthermore, executions are related to other partial-order semantics of nets in much the same way as processes of safe nets are. It is shown that nets are conflict-free (in some sense) if and only if they have just one maximal execution.

Details DOI

MFCS Conference 1990 Conference Paper

Quality Criteria for Partial Order Semantics of Place/Transition-Nets

Robert Gold
Walter Vogler

Abstract This paper discusses a number of properties a partial order semantics should have in order to support the modular construction of nets and to deal with finite capacities. Characterizations for these properties are shown, and a new semantics is introduced which seems to be the natural choice if a certain set of properties is required.

Details

MFCS Conference 1988 Conference Paper

Failures Semantics and Deadlocking of Modular Petri Nets

Walter Vogler

Abstract One can construct labelled P/T -nets in a modular fashion by exchanging subnets such that the behaviour of the whole net remains the same. We investigate which subnets can be exchanged such that deadlock-freeness is preserved and show that some variations of the failures semantics, which has been developed for TCSP, are useful in this context.

Details

MFCS Conference 1988 Conference Paper

Local Checking of Trace Synchroniziability

Volker Diekert
Walter Vogler

Abstract Trace theory has been developed to describe the behaviour of concurrent systems. For a modular approach synchronization of traces is of special interest. We characterize those trace monoids for which synchronization can be described locally.

Details