Foundations of Software Science and Computational Structures

Nominal calculi have been shown very effective to formally model a variety of computational phenomena. The models of nominal calculi have often infinite states, thus making model checking a difficult task. In this note we survey some of the approaches for model checking nominal calculi. Then, we focus on

History-Dependent automata

, a syntax-free automaton-based model of mobility. History-Dependent automata have provided the formal basis to design and implement some existing verification toolkits. We then introduce a novel syntax-free setting to model the symbolic semantics of a nominal calculus. Our approach relies on the notions of reactive systems and observed borrowed contexts introduced by Leifer and Milner, and further developed by Sassone, Lack and Sobocinski. We argue that the symbolic semantics model based on borrowed contexts can be conveniently applied to web service discovery and binding.

The general aim of this talk is to advocate a combinatorial perspective, together with its methods, in the investigation and study of models of computation structures. This, of course, should be taken in conjunction with the well-established views and methods stemming from algebra, category theory, domain theory, logic, type theory,

etc

. In support of this proposal I will show how such an approach leads to interesting connections between various areas of computer science and mathematics; concentrating on one such example in some detail. Specifically, I will consider the line of my research involving denotational models of the pi calculus and algebraic theories with variable-binding operators, indicating how the abstract mathematical structure underlying these models fits with that of Joyal’s combinatorial species of structures. This analysis suggests both the unification and generalisation of models, and in the latter vein I will introduce

generalised species of structures

and their calculus. These generalised species encompass and generalise various of the notions of species used in combinatorics. Furthermore, they have a rich mathematical structure (akin to models of Girard’s linear logic) that can be described purely within Lawvere’s generalised logic. Indeed, I will present and treat the cartesian closed structure, the linear structure, the differential structure,

etc.

of generalised species axiomatically in this mathematical framework. As an upshot, I will observe that the setting allows for interpretations of computational calculi (like the lambda calculus, both typed and untyped; the recently introduced differential lambda calculus of Ehrhard and Regnier;

etc

) that can be directly seen as translations into a more basic elementary calculus of interacting agents that compute by communicating and operating upon structured data.

Structural congruences have been used to define the semantics and to capture inherent properties of language constructs. They have been used as an addendum to transition system specifications in Plotkin’s style of Structural Operational Semantics (SOS). However, there has been little theoretical work on establishing a formal link between these two semantic specification frameworks. In this paper, we give an interpretation of structural congruences inside the transition system specification framework. This way, we extend a number of well-behavedness meta-theorems for SOS (such as well-definedness of the semantics and congruence of bisimilarity) to the extended setting with structural congruences.

We propose an SOS transition rule format for the generative model of probabilistic processes. Transition rules are partitioned in several strata, giving rise to an ordering relation analogous to those introduced by Ulidowski and Phillips for classic process algebras. Our rule format guarantees that probabilistic bisimulation is a congruence w.r.t. process algebra operations. Moreover, our rule format guarantees that process algebra operations preserve semistochasticity of processes, i.e. the property that the sum of the probability of the moves of any process is either 0 or 1. Finally, we show that most of operations of the probabilistic process algebras studied in the literature are captured by our format, which, therefore, has practical applications.

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 one by Lüttgen/Vogler considers upper time bounds instead.

This paper 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.

We study the concept of choice for true concurrency models such as prime event structures and safe Petri nets. We propose a dynamic variation of the notion of cluster previously introduced for nets. This new object is defined for event structures, it is called a

branching cell

. Our aim is to bring an interpretation of branching cells as a right notion of “local state”, for concurrent systems.

We illustrate the above claim through applications to probabilistic concurrent models. In this respect, our results extends in part previous work by Varacca-Völzer-Winskel on probabilistic confusion free event structures. We propose a construction for probabilities over so-called

locally finite

event structures that makes concurrent processes probabilistically independent—simply attach a dice to each branching cell; dices attached to

concurrent

branching cells are thrown independently. Furthermore, we provide a true concurrency generalization of Markov chains, called

Markov nets.

Unlike in existing variants of stochastic Petri nets, our approach randomizes Mazurkiewicz traces, not firing sequences. We show in this context the Law of Large Numbers (LLN), which confirms that branching cells deserve the status of local state.

Our study was motivated by the stochastic modeling of fault propagation and alarm correlation in telecommunications networks and services. It provides the foundations for probabilistic diagnosis, as well as the statistical distributed learning of such models.

We study a process calculus which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch’s probabilistic automata. We consider various strong and weak behavioral equivalences, and we provide complete axiomatizations for finite-state processes, restricted to guarded definitions in case of the weak equivalences. We conjecture that in the general case of unguarded recursion the “natural” weak equivalences are undecidable.

This is the first work, to our knowledge, that provides a complete axiomatization for weak equivalences in the presence of recursion and both nondeterministic and probabilistic choice.

We study the interaction between non-deterministic and probabilistic behaviour in systems with continuous state spaces, arbitrary probability distributions and uncountable branching. Models of such systems have been proposed previously. Here, we introduce a model that extends probabilistic automata to the continuous setting. We identify the class of schedulers that ensures measurability properties on executions, and show that such measurability properties are preserved by parallel composition. Finally, we demonstrate how these results allow us to define an alternative notion of weak bisimulation in our model.

We consider model-checking algorithms for durational probabilistic systems, which are systems exhibiting nondeterministic, probabilistic and discrete-timed behaviour. We present two semantics for durational probabilistic systems, and show how formulae of the probabilistic and timed temporal logic

Ptctl

can be verified on such systems. We also address complexity issues, in particular identifying the cases in which model checking durational probabilistic systems is harder than verifying non-probabilistic durational systems.

The finite

π

-calculus has an explicit set-theoretic functor-category model that is known to be fully abstract for strong late bisimulation congruence. We characterize this as the initial free algebra for an appropriate set of operations and equations in the enriched Lawvere theories of Plotkin and Power. Thus we obtain a novel algebraic description for models of the

π

-calculus, and validate an existing construction as the universal such model.

The algebraic operations are intuitive, covering name creation, communication of names over channels, and nondeterminism; the equations then combine these features in a modular fashion. We work in an enriched setting, over a “possible worlds” category of sets indexed by available names. This expands significantly on the classical notion of algebraic theories, and in particular allows us to use nonstandard arities that vary as processes evolve.

Based on our algebraic theory we describe a category of models for the

π

-calculus, and show that they all preserve bisimulation congruence. We develop a direct construction of free models in this category; and generalise previous results to prove that all free-algebra models are fully abstract.

We investigate a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular cases of the more general notion of

distinction

. The key aspect of this model is to consider functors over the category of irreflexive, symmetric finite relations. The models previously proposed for the notions of “variables” and “names” embed faithfully in the new one, and initial algebra/final coalgebra constructions can be transferred from the formers to the latter. Moreover, the new model admits a definition of

distinction-aware

simultaneous substitutions. As a substantial application example, we give the first semantic interpretation of Miller-Tiu’s

$FO\lambda^{\nabla}$

logic.

We show how parallel composition of higher-dimensional automata (HDA) can be expressed categorically in the spirit of Winskel & Nielsen. Employing the notion of computation path introduced by van Glabbeek, we define a new notion of bisimulation of HDA using open maps. We derive a connection between computation paths and carrier sequences of dipaths and show that bisimilarity of HDA can be decided by the use of geometric techniques.

The problems of contextual equivalence and approximation are studied for the third-order fragment of Idealized Algol with iteration (

IA

$^*_{3}$

). They are approached via a combination of game semantics and language theory. It is shown that for each (

IA

$^{*}_{3}$

)-term one can construct a pushdown automaton recognizing a representation of the strategy induced by the term. The automata have some additional properties ensuring that the associated equivalence and inclusion problems are solvable in

Ptime

. This gives an

Exptime

decision procedure for contextual equivalence and approximation for

β

-normal terms.

Exptime

-hardness is also shown in this case, even in the absence of iteration.

Fault diagnosis consists in observing behaviours of systems, and in detecting

online

whether an error has occurred or not. In the context of discrete event systems this problem has been well-studied, but much less work has been done in the timed framework. In this paper, we consider the problem of diagnosing faults in behaviours of timed plants. We focus on the problem of synthesizing fault diagnosers which are realizable as deterministic timed automata, with the motivation that such diagnosers would function as efficient online fault detectors. We study two classes of such mechanisms, the class of deterministic timed automata (DTA) and the class of event-recording timed automata (ERA). We show that the problem of synthesizing diagnosers in each of these classes is decidable, provided we are given a bound on the resources available to the diagnoser. We prove that under this assumption diagnosability is 2EXPTIME-complete in the case of DTA’s whereas it becomes PSPACE-complete for ERA’s.

In this paper, we prove decidability of the optimal conditional reachability problem for multi-priced timed automata, an extension of timed automata with multiple cost variables evolving according to given rates for each location. More precisely, we consider the problem of determining the minimal cost of reaching a given target state, with respect to some primary cost variable, while respecting upper bound constraints on the remaining (secondary) cost variables. Decidability is proven by constructing a zone-based algorithm that always terminates while synthesizing the optimal cost with a single secondary cost variable. The approach is then lifted to any number of secondary cost variables.

A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem. This gives a new class of timed languages which is closed under boolean operations and which has an effective presentation. We prove that the complexity of the emptiness problem for alternating timed automata with one clock is non-primitive recursive. The proof gives also the same lower bound for the universality problem for nondeterministic timed automata with one clock thereby answering a question asked in a recent paper by Ouaknine and Worrell.

The problem of finding a fully abstract model for the polymorphic

π

-calculus was stated in Pierce and Sangiorgi’s work in 1997 and has remained open since then. In this paper, we show that a slight variant of their language has a direct fully abstract model, which does not depend on type unification or logical relations. This is the first fully abstract model for a polymorphic concurrent language. In addition, we discuss the relationship between our work and Pierce and Sangiorgi’s, and show that their conjectured fully abstract model is, in fact, sound but not complete.

A timed extension of

π

-calculus with a transaction construct – the calculus

Web

π

– is studied. The underlying model of

Web

π

relies on networks of processes; time proceeds asynchronously at the network level, while it is constrained by the

local urgency

at the process level. Namely process reductions cannot be delayed to favour idle steps. The extensional model – the

timed bisimilarity

– copes with time and asynchrony in a different way with respect to previous proposals. In particular, the discriminating power of timed bisimilarity is weaker when local urgency is dropped. A labelled characterization of timed bisimilarity is also discussed.

Language-based and process calculi-based information security are well developed fields of computer security. Although these fields have much in common, it is somewhat surprising that the literature lacks a comprehensive account of a formal link between the two disciplines. This paper develops such a link between a language-based specification of security and a process-algebraic framework for security properties. Encoding imperative programs into a CCS-like process calculus, we show that timing-sensitive security for these programs exactly corresponds to the well understood process-algebraic security property of persistent bisimulation-based nondeducibility on compositions (

P

_

BNDC

). This rigorous connection opens up possibilities for cross-fertilization, leading to both flexible policies when specifying the security of heterogeneous systems and to a synergy of techniques for enforcing security specifications.

An extension of the

λ

-calculus is proposed, to study history-based access control. It allows for security policies with a possibly nested, local scope. We define a type and effect system that, given a program, extracts a history expression, i.e. a correct approximation to the set of histories obtainable at run-time. Validity of history expressions is non-regular, because the scope of policies can be nested. Nevertheless, a transformation of history expressions is presented, that makes verification possible through standard model checking techniques. A program will never fail at run-time if its history expression, extracted at compile-time, is valid.

The idea of composition and decomposition to obtain computability results is particularly relevant for true-concurrency. In contrast to the interleaving world, where composition and decomposition must be considered with respect to a process algebra operator, e.g. parallel composition, we can directly recognize whether a truly-concurrent model such as a labelled asynchronous transition system or a 1-safe Petri net can be dissected into independent ‘chunks of behaviour’. In this paper we introduce the corresponding concept ‘decomposition into independent components’, and investigate how it translates into truly-concurrent bisimulation equivalences. We prove that, under a natural restriction, history preserving (hp), hereditary hp (hhp), and coherent hhp (chhp) bisimilarity are decomposable with respect to prime decompositions. Apart from giving a general proof technique our decomposition theory leads to several coincidence results. In particular, we resolve that hp, hhp, and chhp bisimilarity coincide for ‘normal form’ basic parallel processes.

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.

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 it is shown that speed-independent CSC solving preserves correctness. The latter uses a more general result about correctness of top-down decomposition. Furthermore, we apply our definition to give the first correctness proof for the decomposition method of Carmona and Cortadella.

We are interested in implementing a fully automated software development process starting from sequence charts, which have proven their naturalness and usefulness in industry. We show in this paper that even for the simplest variants of sequence charts, there are strong impediments to the implementability of this dream. In the case of a manual development, we have to check the final implementation (the model). We show that centralized model-checking is co-NP-complete. Unfortunately, this problem is of little interest to industry. The real problem is distributed model-checking, that we show PSPACE complete, as well as several simple but interesting verification problems. The dream itself relies on program synthesis, formally called realizability. We show that the industrially relevant problem, distributed realizability, is undecidable. The less interesting problems of centralized and constrained realizability are exponential and doubly-exponential complete, respectively.

Nominal logic is a variant of first-order logic equipped with a “fresh-name quantifier”

И

and other features useful for reasoning about languages with bound names. Its original presentation was as a Hilbert axiomatic theory, but several attempts have been made to provide more convenient Gentzen-style sequent or natural deduction calculi for nominal logic. Unfortunately, the rules for

И

in these calculi involve complicated side-conditions, so using and proving properties of these calculi is difficult. This paper presents an improved sequent calculus

NL

⇒

for nominal logic. Basic results such as cut-elimination and conservativity with respect to nominal logic are proved. Also,

NL

⇒

is used to solve an open problem, namely relating nominal logic’s

И

-quantifier and the self-dual

$\nabla$

-quantifier of Miller and Tiu’s

$FO\lambda^{\nabla}$

.

Separation logic is a spatial logic for reasoning locally about heap structures. A decidable fragment of its assertion language was presented in [1], based on a bounded model property. We exploit this property to give an encoding of this fragment into a first-order logic containing only the propositional connectives, quantification over the natural numbers and equality. This result is the first translation from Separation Logic into a logic which does not depend on the heap, and provides a direct decision procedure based on well-studied algorithms for first-order logic. Moreover, our translation is compositional in the structure of formulae, whilst previous results involved enumerating either heaps or formulae arising from the bounded model property.

Deciding the typing judgement of type theories with dependent types such as the Logical Framework relies on deciding the equality judgement for the same theory. Implementing the conversion algorithm for

βη

-equality and justifying this algorithm is therefore an important problem for applications such as proof assistants and modules systems. This article gives a proof of decidability, correctness and completeness of the conversion algorithms for

βη

-equality defined by Coquand [3] and Harper and Pfenning [8] for the Logical Framework, relying on established metatheoretic results for the type theory. Proofs are also given of the same properties for a typed algorithm for conversion for System F, a new result.

The arithmetic of natural numbers with addition and divisibility has been shown undecidable as a consequence of the fact that multiplication of natural numbers can be interpreted into this theory, as shown by J. Robinson [14]. The most important decidable subsets of the arithmetic of addition and divisibility are the arithmetic of addition, proved by M. Presburger [13], and the purely existential subset, proved by L. Lipshitz [11]. In this paper we define a new decidable fragment of the form

QzQ

1

x

1

...

Q

n

x

n

ϕ

(

x

,

z

) where the only variable allowed to occur to the left of the divisibility sign is

z

. For this form, called

${\mathcal L}{_{\mid}^{(1)}}$

in the paper, we show the existence of a quantifier elimination procedure which always leads to formulas of Presburger arithmetic. We generalize the

${\mathcal L}{_{\mid}^{(1)}}$

form to ∃ 

z

1

,... ∃ 

z

m

Q

1

x

1

...

Q

n

x

n

ϕ

(

x

,

z

), where the only variables appearing on the left of divisibility are

z

1

, ...,

z

m

. For this form, called

$\exists{\mathcal L}{_{\mid}^{(*)}}$

, we show decidability of the positive fragment, namely by reduction to the existential theory of the arithmetic with addition and divisibility. The

${\mathcal L}{_{\mid}^{(1)}}$

,

$\exists{\mathcal L}{_{\mid}^{(*)}}$

fragments were inspired by a real application in the field of program verification. We considered the satisfiability problem for a program logic used for quantitative reasoning about memory shapes, in the case where each record has at most one pointer field. The reduction of this problem to the positive subset of

$\exists{\mathcal L}{_{\mid}^{(*)}}$

is sketched in the end of the paper.

Modal logic has a good claim to being the logic of choice for describing the reactive behaviour of systems modeled as coalgebras. Logics with modal operators obtained from so-called predicate liftings have been shown to be invariant under behavioral equivalence. Expressivity results stating that, conversely, logically indistinguishable states are behaviorally equivalent depend on the existence of separating sets of predicate liftings for the signature functor at hand. Here, we provide a classification result for predicate liftings which leads to an easy criterion for the existence of such separating sets, and we give simple examples of functors that fail to admit expressive normal or monotone modal logics, respectively, or in fact an expressive (unary) modal logic at all. We then move on to polyadic modal logic, where modal operators may take more than one argument formula. We show that every accessible functor admits an expressive polyadic modal logic. Moreover, expressive polyadic modal logics are, unlike unary modal logics, compositional.

We present a general framework for logics of transition systems based on Stone duality. Transition systems are modelled as coalgebras for a functor

T

on a category

χ

. The propositional logic used to reason about state spaces from

χ

is modelled by the Stone dual

${\mathcal A}$

of

χ

(e.g. if

χ

is Stone spaces then

${\mathcal A}$

is Boolean algebras and the propositional logic is the classical one). In order to obtain a modal logic for transition systems (i.e. for

T

-coalgebras) we consider the functor

L

on

${\mathcal A}$

that is dual to

T

. An adequate modal logic for

T

-coalgebras is then obtained from the category of

L

-algebras which is, by construction, dual to the category of

T

-coalgebras. The logical meaning of the duality is that the logic is sound and complete and expressive (or fully abstract) in the sense that non-bisimilar states are distinguished by some formula.

We apply the framework to Vietoris coalgebras on topological spaces, using the duality between spaces and observation frames, to obtain adequate logics for transition systems on posets, sets, spectral spaces and Stone spaces.

Term rewriting systems provide a versatile model of computation. An important property which allows to abstract from potential nondeterminism of parallel execution of the modelled program is confluence. In this paper we prove that confluence of a fairly large class of systems, namely right ground term rewriting systems, is decidable. We introduce a labelling of variables with colours and constrain substitutions according to these colours. We show how right ground rewriting systems can be reduced to simple systems with coloured variables. Such systems can be analysed using reduction-automata techniques which leads to an interesting decision procedure for confluence.

Recent work by Knapik, Niwiński and Urzyczyn (in FOSSACS 2002) has revived interest in the connexions between higher-order grammars and higher-order pushdown automata. Both devices can be viewed as definitions for term trees as well as string languages. In the latter setting we recall the extensive study by Damm (1982), and Damm and Goerdt (1986). There it was shown that a language is accepted by a level-

n

pushdown automaton if and only if the language is generated by a

safe

level-

n

grammar. We show that at level 2 the safety assumption may be removed. It follows that there are no

inherently

unsafe string languages at level 2.

We introduce a domain-theoretic computational model for multi-variable differential calculus, which for the first time gives rise to data types for differentiable functions. The model, a continuous Scott domain for differentiable functions of

n

variables, is built as a sub-domain of the product of

n

+ 1 copies of the function space on the domain of intervals by tupling together consistent information about locally Lipschitz (piecewise differentiable) functions and their differential properties (partial derivatives). The main result of the paper is to show, in two stages, that consistency is decidable on basis elements, which implies that the domain can be given an effective structure. First, a domain-theoretic notion of line integral is used to extend Green’s theorem to interval-valued vector fields and show that integrability of the derivative information is decidable. Then, we use techniques from the theory of minimal surfaces to construct the least and the greatest piecewise linear functions that can be obtained from a tuple of

n

+ 1 rational step functions, assuming the integrability of the

n

-tuple of the derivative part. This provides an algorithm to check consistency on the rational basis elements of the domain, giving an effective framework for multi-variable differential calculus.