BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Uwe Nestmann

Uwe Nestmann appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceFormal Languages and Automata Theory

Catalog footprint

What is connected

12works
2topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

12 published item(s)

preprint2015arXiv

Dynamic Causality in Event Structures (Technical Report)

In [1] we present an extension of Prime Event Structures by a mechanism to express dynamicity in the causal relation. More precisely we add the possibility that the occurrence of an event can add or remove causal dependencies between events and analyse the expressive power of the resulting Event Structures w.r.t. to some well-known Event Structures from the literature. This technical report contains some additional information and the missing proofs of [1].

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Encoding CSP into CCS

We study encodings from CSP into asynchronous CCS with name passing and matching, so in fact, the asynchronous pi-calculus. By doing so, we discuss two different ways to map the multi-way synchronisation mechanism of CSP into the two-way synchronisation mechanism of CCS. Both encodings satisfy the criteria of Gorla except for compositionality, as both use an additional top-level context. Following the work of Parrow and Sjödin, the first encoding uses a centralised coordinator and establishes a variant of weak bisimilarity between source terms and their translations. The second encoding is decentralised, and thus more efficient, but ensures only a form of coupled similarity between source terms and their translations.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Encoding CSP into CCS (Extended Version)

We study encodings from CSP into asynchronous CCS with name passing and matching, so in fact, the asynchronous pi-calculus. By doing so, we discuss two different ways to map the multi-way synchronisation mechanism of CSP into the two-way synchronisation mechanism of CCS. Both encodings satisfy the criteria of Gorla except for compositionality, as both use an additional top-level context. Following the work of Parrow and Sjödin, the first encoding uses a central coordinator and establishes a variant of weak bisimilarity between source terms and their translations. The second encoding is decentralised, and thus more efficient, but ensures only a form of coupled similarity between source terms and their translations.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Enforcing Operational Properties including Blockfreeness for Deterministic Pushdown Automata

We present an algorithm which modifies a deterministic pushdown automaton (DPDA) such that (i) the marked language is preserved, (ii) lifelocks are removed, (iii) deadlocks are removed, (iv) all states and edges are accessible, and (v) operational blockfreeness is established (i.e., coaccessibility in the sense that every initial derivation can be continued to a marking configuration). This problem can be trivially solved for deterministic finite automata (DFA) but is not solvable for standard petri net classes. The algorithm is required for an operational extension of the supervisory control problem (SCP) to the situation where the specification in modeled by a DPDA.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Matching in the Pi-Calculus

We study whether, in the pi-calculus, the match prefix-a conditional operator testing two names for (syntactic) equality-is expressible via the other operators. Previously, Carbone and Maffeis proved that matching is not expressible this way under rather strong requirements (preservation and reflection of observables). Later on, Gorla developed a by now widely-tested set of criteria for encodings that allows much more freedom (e.g. instead of direct translations of observables it allows comparison of calculi with respect to reachability of successful states). In this paper, we offer a considerably stronger separation result on the non-expressibility of matching using only Gorla's relaxed requirements.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Matching in the Pi-Calculus (Technical Report)

We study whether, in the pi-calculus, the match prefix---a conditional operator testing two names for (syntactic) equality---is expressible via the other operators. Previously, Carbone and Maffeis proved that matching is not expressible this way under rather strong requirements (preservation and reflection of observables). Later on, Gorla developed a by now widely-tested set of criteria for encodings that allows much more freedom (e.g. instead of direct translations of observables it allows comparison of calculi with respect to reachability of successful states). In this paper, we offer a considerably stronger separation result on the non-expressibility of matching using only Gorla's relaxed requirements.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

States in Process Calculi

Formal reasoning about distributed algorithms (like Consensus) typically requires to analyze global states in a traditional state-based style. This is in contrast to the traditional action-based reasoning of process calculi. Nevertheless, we use domain-specific variants of the latter, as they are convenient modeling languages in which the local code of processes can be programmed explicitly, with the local state information usually managed via parameter lists of process constants. However, domain-specific process calculi are often equipped with (unlabeled) reduction semantics, building upon a rich and convenient notion of structural congruence. Unfortunately, the price for this convenience is that the analysis is cumbersome: the set of reachable states is modulo structural congruence, and the processes' state information is very hard to identify. We extract from congruence classes of reachable states individual state-informative representatives that we supply with a proper formal semantics. As a result, we can now freely switch between the process calculus terms and their representatives, and we can use the stateful representatives to perform assertional reasoning on process calculus models.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Adding Priority to Event Structures

Event Structures (ESs) are mainly concerned with the representation of causal relationships between events, usually accompanied by other event relations capturing conflicts and disabling. Among the most prominent variants of ESs are Prime ESs, Bundle ESs, Stable ESs, and Dual ESs, which differ in their causality models and event relations. Yet, some application domains require further kinds of relations between events. Here, we add the possibility to express priority relationships among events. We exemplify our approach on Prime, Bundle, Extended Bundle, and Dual ESs. Technically, we enhance these variants in the same way. For each variant, we then study the interference between priority and the other event relations. From this, we extract the redundant priority pairs-notably differing for the types of ESs-that enable us to provide a comparison between the extensions. We also exhibit that priority considerably complicates the definition of partial orders in ESs.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Synchrony vs Causality in the Asynchronous Pi-Calculus

We study the relation between process calculi that differ in their either synchronous or asynchronous interaction mechanism. Concretely, we are interested in the conditions under which synchronous interaction can be implemented using just asynchronous interactions in the pi-calculus. We assume a number of minimal conditions referring to the work of Gorla: a "good" encoding must be compositional and preserve and reflect computations, deadlocks, divergence, and success. Under these conditions, we show that it is not possible to encode synchronous interactions without introducing additional causal dependencies in the translation.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Breaking Symmetries

A well-known result by Palamidessi tells us that πmix (the π-calculus with mixed choice) is more expressive than πsep (its subset with only separate choice). The proof of this result argues with their different expressive power concerning leader election in symmetric networks. Later on, Gorla of- fered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of "incestual" processes (mixed choices that include both enabled senders and receivers for the same channel) when running two copies in parallel. In both proofs, the role of breaking (ini- tial) symmetries is more or less apparent. In this paper, we shed more light on this role by re-proving the above result-based on a proper formalization of what it means to break symmetries-without referring to another layer of the distinguishing problem domain of leader election. Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reason- able encoding from πmix into πsep . We indicate how the respective proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Breaking Symmetries

A well-known result by Palamidessi tells us that \pimix (the π-calculus with mixed choice) is more expressive than \pisep (its subset with only separate choice). The proof of this result argues with their different expressive power concerning leader election in symmetric networks. Later on, Gorla offered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of incestual processes (mixed choices that include both enabled senders and receivers for the same channel) when running two copies in parallel. In both proofs, the role of breaking (initial) symmetries is more or less apparent. In this paper, we shed more light on this role by re-proving the above result - based on a proper formalization of what it means to break symmetries without referring to another layer of the distinguishing problem domain of leader election. Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from \pimix into \pisep. We indicate how the respective proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential.

0 citations0 reviewsNo code linkedOpen access