Concurrency

Checking marking reachability with the state equation in Petri net subclasses

Although decidable, the marking reachability problem for Petri nets is well-known to be intractable in general, and a non-elementary lower bound has been recently uncovered. In order to alleviate this difficulty, various structural …

On the Petri Nets with a Single Shared Place and Beyond

Petri nets proved useful to describe various real-world systems, but many of their properties are very hard to check. To alleviate this difficulty, subclasses are often considered. The class of weighted marked graphs with relaxed place constraint …

TraLaLa

Nov 2004 — Feb 2008. TraLaLA, XML Transformation Languages: logic and applications, is a project funded by ACI MASSES DE DONNÉES. The objectives of the project is to study the processing, querying and manipulation of _data-masses_ (large amounts of data) available in XML format.

A Typed Calculus for Querying Distributed XML Documents

We study the problems related to querying large, distributed XML documents. Our proposal takes the form of a new process calculus in which XML data are processes that can be queried by means of concurrent pattern-matching …

A Typed Calculus for Querying Distributed XML Documents

We study the problems related to querying large, distributed XML documents. Our proposal takes the form of a new process calculus in which XML data are processes that can be queried by means of concurrent pattern-matching …

On the Dynamics of PB Systems: A Petri Net View

We study dynamical properties of PB systems, a new computational model of biological processes, and propose a compositional encoding of PB systems into Petri nets. Building on this relation, we show that three properties: …

Model Checking Mobile Ambients

We settle the complexity bounds of the model checking problem for the ambient calculus with public names against the ambient logic. We show that if either the calculus contains replication or the logic contains the guarantee …

Region analysis and a pi-calculus with groups

We show that the typed region calculus of Tofte and Talpin can be encoded in a typed pi-calculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in …

Fixed Points in the Ambient Logic

We present an extension of the ambient logic with fixed points operators in the style of the μ-calculus. We give a simple syntactic condition for the equivalence between minimal and maximal fixpoint formulas and show how to subsume …

Mobile Processes: a Commented Bibliography

We propose a short bibliographic survey of calculi for mobile processes. Contrasting with other similar exercises, we consider two related, but distinct, notions of mobile processes, namely labile processes, which can exhibit …