Search

Propositional dynamic logic is extended with a parallel program having a separating semantic: the program \((\alpha \parallel \beta )\) executes \(\alpha \) and \(\beta \) on two substates of the current state. We prove that when the composition of two substates is deterministic, the logic has the exponential-size model property. The proof is by a piecewise filtration using an adaptation of the Fischer-Ladner closure. We conclude that the satisfiability of the logic is decidable in NEXPTIME.

We integrate, and improve upon, prior relative soundness results of two kinds. The first kind are typing results showing that any security protocol that fulfils a number of sufficient conditions has an attack if it has a well-typed attack. The second kind considers the parallel composition of protocols, showing that when running two protocols in parallel allows for an attack, then at least one of the protocols has an attack in isolation. The most important generalization over previous work is the support for all security properties of the geometric fragment.

Man-in-the-Middle (MM) is not only a ubiquitous attack pattern in security, but also an important paradigm of network computation and economics. Recognizing ongoing MM-attacks is an important security task; modeling MM-interactions is an interesting task for semantics of computation. Traced monoidal categories are a natural framework for MM-modelling, as the trace structure provides a tool to hide what happens in the middle. An effective analysis of what has been traced out seems to require an additional property of traces, called normality. We describe a modest model of network computation, based on partially ordered multisets (pomsets), where basic network interactions arise from the monoidal trace structure, and a normal trace structure arises from an iterative, i.e. coalgebraic structure over terms and messages used in computation and communication. The correspondence is established using a convenient monadic description of normally traced monoidal categories.

During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi. During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi.

A language for representing timed automata is introduced. Its semantics is defined in terms of timed automata. This language is complete in the sense that any timed automaton can be represented by a term in the language. We also define a direct operational semantics for the language in terms of (timed) transition systems. This is proven to be equivalent (or, more precisely, timed bisimilar) to the interpretation in terms of timed automata. In addition, a set of axioms is given that is shown to be sound for timed bisimulation. Finally, we introduce several features including the parallel composition and derived time operations like wait, time-out and urgency. We conclude with an example and show that we can eliminate non-reachable states using algebraic techniques.

There are now several theories for describing and reasoning about the behavior of communicating systems, where the behavior of a communicating system is described in terms of its capabilities to perform communication actions in cooperation with its environment. In such theories, preorders or equivalences are defined as criteria for when one system is an acceptable substitute or implementation of another. Existing theories of communicating systems define preorders or equivalence relations only between systems with identical sets of communication actions. In many practical design situations, however, it may be desirable to refine a system by changing its set of communication actions. We present a simple method for carrying out such refinements. The method is first formulated in a general setting, and then elaborated in more detail in the trace model and a simple version of the failure model. We illustrate the usefulness of our method by an application to I.451, an ISDN access protocol.