Browse Proceedings

In this paper we introduce a real-time extension of the concurrent object modeling language Creol which is based on duration statements indicating best and worst case execution times and deadlines. We show how to analyze schedulability of an abstraction ...

We discuss conceptional and foundational aspects of Markov automata [22]. We place this model in the context of continuous- and discrete-time Markov chains, probabilistic automata and interactive Markov chains, and provide insight into the parallel ...

This extended abstract surveys some analysis techniques for distributed, asynchronous systems with two kinds of synchronization, shared variables and fifo channels.

Anonymity is a security property of paramount importance, as we move steadily towards a wired, online community. Its import touches upon subjects as different as eGovernance, eBusiness and eLeisure, as well as personal freedom of speech in authoritarian ...

Links are established between three widely used modeling frameworks for reactive systems: the ioco theory of Tretmans, the interface automata of De Alfaro and Henzinger, and Mealy machines. It is shown that, by exploiting these links, any tool for ...

In this paper, we develop a counterexample-guided abstraction refinement (CEGAR) framework for monotonic abstraction, an approach that is particularly useful in automatic verification of safety properties for parameterized systems. The main drawback of ...

We consider the problem of defining the information leakage in interactive systems where secrets and observables can alternate during the computation. We show that the information-theoretic approach which interprets such systems as (simple) noisy ...

We investigate the issue of reducing the verification problem of multistack machines to the one for single-stack machines. For instance, elegant (and practically efficient) algorithms for bounded-context switch analysis of multipushdown systems have ...

This paper proposes a geometric solution to the problem of prime decomposability of concurrent processes first explored by R. Milner and F. Moller in [MM93]. Concurrent programs are given a geometric semantics using cubical areas, for which a unique ...

We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history preserving bisimilarity, and fragments of the logic can be identified ...

Design by Contract (DbC) promotes reliable software development through elaboration of type signatures for sequential programs with logical predicates. This paper presents an assertion method, based on the π-calculus with full recursion, which ...

A one-counter automaton is a pushdown automaton over a singleton stack alphabet. We prove that the bisimilarity of processes generated by nondeterministic one-counter automata (with no ε-steps) is in PSPACE. This improves the previously known ...

We propose a procedure for computing Nash equilibria in multi-player timed games with reachability objectives. Our procedure is based on the construction of a finite concurrent game, and on a generic characterization of Nash equilibria in (possibly ...

We consider two-player stochastic games over real-time probabilistic processes where the winning objective is specified by a timed automaton. The goal of player □ is to play in such a way that the play (a timed word) is accepted by the timed automaton ...

Several type disciplines for π-calculi have been proposed in which linearity plays a key role, even if their precise relationship with pure linear logic is still not well understood. In this paper, we introduce a type system for the π-calculus that ...

We consider a calculus for multiparty sessions with delegation, enriched with security levels for session participants and data. We propose a type system that guarantees both session safety and a form of access control. Moreover, this type system ...

Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by realvalued distance functions between systems, where the distance between implementation and specification provides a ...

Quantitative languages are an extension of boolean languages that assign to each word a real number. Mean-payoff automata are finite automata with numerical weights on transitions that assign to each infinite path the long-run average of the transition ...

Graph games of infinite length provide a natural model for open reactive systems: one player (Eve) represents the controller and the other player (Adam) represents the environment. The evolution of the system depends on the decisions of both players. ...

We study generalized simulation relations for alternating Büchi automata (ABA), as well as alternating finite automata. Having multiple pebbles allows the Duplicator to "hedge her bets" and delay decisions in the simulation game, thus yielding a coarser ...

We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with selective broadcast and spontaneous movement. The communication topology of a network is represented as a graph. Nodes represent states of individual ...

An impure language is one that combines functional and imperative constructs. We propose a method for ensuring termination of impure concurrent languages that makes it possible to combine term rewriting measure-based techniques with traditional ...

Many communication-centred systems today rely on asynchronous messaging among distributed peers to make efficient use of parallel execution and resource access.With such asynchrony, the communication buffers can happen to grow inconsiderately over time. ...

We investigate Leifer and Milner RPO approach for deriving efficient (finitely branching) LTS's and bisimilarities for p-calculus. To this aim, we work in a category of second-order term contexts and we apply a general pruning technique, which allows to ...

A well-known decision procedure for Presburger arithmetic uses deterministic finite-state automata. While the complexity of the decision procedure for Presburger arithmetic based on quantifier elimination is known (roughly, there is a double-exponential ...

Optimistic concurrency algorithms provide good performance for parallel programs but they are extremely hard to reason about. Program logics such as concurrent separation logic and rely-guarantee reasoning can be used to verify these algorithms, but ...

Theories defined in a process model are formalized and studied. A theory in a process calculus is a set of perpetually available processes with finite interactability, each can be regarded as a service, an agent behind the scene or an axiom. The ...

We revisit a technique called round abstraction as a solution to the problem of building low-latency synchronous systems from asynchronous specifications. We use a trace-semantic setting akin to Abramsky's Interaction Categories, which is also a ...

We present a reconstruction of session types in a conventional pi calculus where types are qualified as linear or unrestricted. Linearly typed communication channels are guaranteed to occur in exactly one thread, possibly multiple times. We equip types ...