Eighteenth Workshop on the Mathematical Foundations of Programming Semantics

Abstracts

Invited Talks

Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state discrete programs. This talk discusses algorithms and tools for reachability analysis of hybrid systems by combining the notion of predicate abstraction with recent techniques for approximating the set of reachable states of linear systems using polyhedra. Given a  hybrid system and a set of user-defined boolean predicates, we consider the finite discrete quotient whose states correspond to the all possible truth assignments to the input predicates. The tool performs an on-the-fly exploration of the abstract system by using weakest preconditions to compute abstract transitions corresponding to the discrete switches and conservative polyhedral approximations to compute abstract transitions corresponding to continuous flows. Compared to tools such as Checkmate and d/dt, this approach requires significantly less computational resources as the emphasis is shifted from computing the reachable set to searching in the abstract quotient. We demonstrate the utility of the proposed technique by analyzing controllers from automotive applications.

We rapidly introduce elements of abstract interpretation, a formalization of the (effective) conservative approximation of the semantics of programs and more generally software and hardware computer systems.
We argue that most semantics-based reasonings and computations on programs involve conservative approximations which are naturally formalized by abstract interpretation. This is illustrated on the syntax and semantics of programming languages, typing and type inference, program transformation, model-checking and static program analysis.

Finite-state verification techniques, such as model checking, have been an effective means for finding subtle defects in hardware designs. The increased use of concurrent software in embedded applications and the widespread adoption of Java with its built-in concurrency constructs have led researchers to attempt to adapt model-checking techniques to software.  To date, this effort has been hindered by several obstacles including construction of correct tractable models from programs with enormous state spaces, appropriate specification of checkable software requirements, and interpretation of very long counterexample traces.

In this talk, we describe Bandera -- an integrated collection of tools for model-checking concurrent Java software that attempts to overcome the obstacles described above.  Bandera is a model compiler in the sense that it takes Java source code as input and compiles it to a program model expressed in the input language of one of several existing verification tools including SMV, Spin, dSpin, and JPF.  Program slicing and abstract interpretation components are used during compilation to customize the program model with respect to the properties being checked. Bandera is like a debugger in the sense that it maps counterexamples produced by back-end model checkers back to the source code level, and it allows the user to replay program execution both forwards and backwards along the path of the counterexample.

We illustrate the functionality Bandera's major components with some simple examples and give an overview of how Bandera's extensible temporal property specification language can be used to specify temporal properties in terms of Java source code features.  We conclude with a discussion of other forms of automated tool support that we are currently working on that we believe are necessary for model-checking properties of large code bases.

There are at least three kinds of behavior on the Internet: honest compliance with standard protocols, destructive non-compliance, and rational profit-maximizing self interest. Historically, Internet protocols were defined under the assumption that routers and nodes would compy with protocol standards. Computer security is generally concerned with behavior that is destructive to others, without serving any obvious goal for the attacker. Traditional economic theory analyzes rational behavior that maximizes some form of profit or wellfare.

In this talk, we will discuss some network problems, such as congestion control and interdomain network routing, where rational self interest may lead agents not to comply with protocol standards. For these problems, we aim to develop mechanisms that will provide good global performance when local behavior is profit maximizing. In a variation on standard mechamism design, we also look at ways to use the extra information associated with these mechansims to improve security against malicious and potentially irrational attacks.

Traditional mechanism design involves the design of pricing functions to encourage desired behavior. Recent interest in algorithmic mechanism design, which recognizes the computational limits of participating agents, has led to increasing interest in applications of mechanism design to electronic commerce and computer science.

In joint work with Peter O'Hearn and Hongseok Yang, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about shared mutable data structure, and possibly other kinds of shared resources.

The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage.  Assertions are extended by introducing an "separating conjunction" operation that asserts that its subformulas hold for disjoint parts of the heap. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing.

In this talk, we will introduce the basic concepts of our approach, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures.

The Specware/Designware system supports specifying, refining, and reasoning about complex software applications.  The system combines higher-order logical specifications, composition, refinement, and abstract design theories, all couched in a categorical setting.  Applications include complex scheduling algorithms, Java byte code verifier, Java applet generation, mechanical system design, and system composition and refinement.  We show how to extend higher-order logical specifications to evolving specifications (especs) in such a way that composition and refinement operations extend to capture the dynamics of evolving, adaptive, and self-adaptive software development, while remaining efficiently computable.  The framework is partially implemented in the Epoxi extension of Specware.

Special Sessions

Abstract Interpretation

Completeness is a desirable feature of any abstraction, formalizing the intuition that, relatively to the approximated observables, there is no loss of information which is accumulated by approximating computations in the corresponding abstract domain. In this talk we consider the problem of making abstract interpretations complete by minimally refining or simplifying abstract domains. We provide a constructive characterization for the least complete refinement and the greatest complete simplification of abstractions relatively to a forward/backward semantics. We show how this theory can be used to derive both effective algorithms for manipulating and comparing abstract interpretations and to better understand the power and limitations of known abstractions in semantics, program analysis and model-checking. We show that compositional semantics abstracting maximal traces of a transition system can be systematically derived by making the abstraction complete for trace concatenation. Then, starting from Cousot's observation that state-based model-checking is incomplete with respect to the trace-based semantics of an enhanced mu-calculus, we show that there is no way to make it complete unless having traces them self in the model or by considering straightforward abstractions asserting that a trace is a trace. This proves that any state-based model checking is intrinsically incomplete with respect to the trace-based semantics of the mu-calculus. We conclude by giving a constructive characterization of Clarke et al.'s spurious counterexamples in terms of completeness of the underlying abstract interpretation. This result allows us to understand the structure of the counterexamples produced by a model-checker that can be removed by systematically refining abstractions. The results presented in the talk have been obtained jointly with: Isabella Mastroeni, Elisa Quintarelli, Francesco Ranzato, and Francesca Scozzari.

Everybody knows that computers calculate numerical results which are mostly wrong, yet they are intensively used for simulating highly complex physical processes and for predicting their behavior. Transcendental numbers cannot be represented exactly in a computer, since machines only use finite implementations of numbers (floating-point numbers instead of mathematical real numbers); they are truncated to a given number of decimals. Less known is that the usual algebraic laws (associativity for instance) that we use when thinking about numbers are no longer true in general when it comes to manipulating floating-point numbers. I will present in this talk  correct semantics of IEEE754 floating-point numbers together with static analyses through its abstract interpretation (joint work with M. Martel and S. Putot at CEA, under the auspices of EEC project DAEDALUS). The prototype analyzer coming out from this study will be briefly shown on interesting examples, typical from instrumentation and control software.

Most compilers ignore the problems of limited code space in embedded systems. Designers of embedded software often have no better alternative than to manually optimize the source code or even the compiled code. Besides being tedious and error-prone, such manual optimization results in obfuscated code which is difficult to maintain and reuse. In this talk we present a code-size-directed compiler. We phrase register allocation and code generation as an integer linear programming problem where the desired bound on the code size is expressed as an additional constraint. Our experimental results show that our compiler, when applied to two commercial microcontrollers, can generate code that is as compact as carefully crafted code.

Abstract interpretation has been around for a long time and has been used to succesfully solve a variety of program analysis problems. As the field continues to develop, new problems and issues arise. Using our combined pointer and escape analysis as background, we discuss some of these issues and speculate on the role that abstract interpretation will play in the continuing development of program analysis.

Hybrid Systems

A functional type in a programming language provides a static description of the relation between the input and output values of a function. If we allow this relation to change dynamically, we obtain a game. With each state of the game is associated a functional type; at each round of the game, the two players Input and Output choose values that satisfy the local functional type of the state, and the game proceeds to a successor state. As noted by Abramsky, games provide a semantics for interaction: this talk explores the use of games for capturing the dynamic behavior of system components, obtaining a type system for system-level design. In particular, we show that type checking corresponds to game composition, and answers the question "do the components interact in a compatible way?", while subtyping corresponds to game refinement, and answers the question "can one component be substituted for another in a design?". We illustrate the use of games as types with examples from hardware and protocols.

 

  • Radha Jagadeesan, Loyola, Chicago, Approximate reasoning in probabilistic concurrency.

    • Hybrid cc is a synchronous concurrent constraint programming language targeted to the modelling and simulation of hybrid systems.  Hybrid cc has been used for a range of examples including electromechanical systems in model based computing projects (at Parc and Nasa), and biological systems (in the ModBio project at Loria).  Several of these examples motivate, and some incorporate stochastic modeling.

    This talk focuses on the issues that arise out of the integration of probabilities. Robust reasoning in the presence of probability numbers requires the use of reasoning techniques that are not too dependent on the exact numerical values of the probabilities.  We present recent results on metric based approximate reasoning for weak bisimulation in labelled
    concurrent Markov chains.  We describe a fixed point characterization of the metric (to permit coinductive proofs for approximate reasoning) and a real-valued modal logic characterization of the metric.  These results support the thesis that approximate reasoning is no harder than the classical exact reasoning in concurrency theory.

    Hybrid cc is joint work with Bobrow, Gupta and Saraswat.  The study of approximate reasoning for probabilistic systems is joint work with Desharnais, Gupta and Panangaden.

     

    The Phi-calculus is a hybrid extension of Milner's Pi-calculus which allows processes to interact with continuous environments. The key idea is to add an explicit formal model of the active, continuous (physical) environment to an algebraic process description, and to add environmental actions to processes which allow them to explicitly manipulate their environment. In this talk we specify flow transition rules (evolution of the continuous environment over time) and show that weakly bisimilar Phi-processes flow in the same way when placed in the same environment.

    Security Session

    Distributed contract signing over a network involves many challenges in mimicking the features of paper contract signing. For instance, a paper contract is usually signed by both parties at the same time and at the same place, but distributed electronic transactions over a network is inherently asymmetric in that someone has to send the first message.

    Several digital contract-signing protocols have been devised in order to overcome this basic asymmetry and to achieve symmetric properties such as fairness, namely: 1) if nothing goes wrong, both participants receive a valid contract, 2) every participant may complete the protocol, and 3) either both participants receive a valid contract or neither one does. Such protocols often involve a trusted third party that can enforce the contract  after it witnesses a partial completion of the protocol. In optimistic contract-signing protocols the trusted third party is contacted only in case of a dispute, otherwise the protocol can be completed without involving the third party. Such protocols involve several subprotocols that allow a contract to be signed normally or aborted or resolved by the trusted third party.

    Another kind of symmetry desirable in distributed contract signing was identified by Garay, Jakobsson, and MacKenzie: a fair protocol is said to be abuse-free if, at any stage of the protocol, it is impossible for any participant, say A, to be able to prove to an outside challenger that A has the power to choose between completing the contract and aborting it. A formal analysis of the Garay-Jakobsson-MacKenzie two-party contract-signing protocol was carried out by Mitchell and Shmatikov using a finite state verification tool. They showed that negligence of the trusted third party may lead to loss of abuse-freeness or fairness. Based on their analysis, Mitchell and Shmatikov also suggested a revision of the protocol. This revised version is our reference point.

    We study an approximation of the abuse-freeness property, namely, at any stage of a fair protocol, any protocol participant does not have both the power to complete the contract as well as the power to abort it. As noted by Mitchell and Shmatikov, this property is not trace-based. We use a multiset-rewriting formalism for protocol analysis to formally state this property in terms of a certain recursive property of the protocol execution tree, which we then prove
    by inductive methods. Our proof relies on a strong notion of fairness adopted from which itself we formally state in the multiset-rewriting formalism and prove by inductive methods. We also show that our approximation of abuse-freeness, even though it is not a trace-based property, it may nevertheless be represented in by means of provability in a logical system, in the multiplicative additive fragment of linear logic, in which formal derivations
    correspond to full protocol execution trees and vice versa. This work was carried out in collaboration with Max Kanovich and Andre Scedrov.

    We also discuss current work in progress with John Mitchell, Andre Scedrov, and Vitaly Shmatikov. We strengthen the definition of abuse-freeness in two ways. We consider strategies against honest participants interested in completing the contract and whose actions display a bias toward a positive outcome. We suggest a formulation of "evidence to an outside participant" by means of epistemic logic.

    Equational unification can be an effective tool for the analysis of cryptographic protocols. This, for example, is the technique used by the NRL Protocol Analyzer, which uses narrowing to reason about cryptographic operations which can be described in terms of rewrite rules.

    However, the effectiveness of equational unification in cryptographic protocol analysis has been hampered by the lack of unification algorithms that can be used to reason about some of the more equationally rich algorithms used by many cryptographic systems, such as Diffie-Hellman, group Diffie-Hellman, and blinded signatures.


    In this paper we attempt to close this gap by providing an algorithm that can be used to reason about protocols that use the Diffie-Hellman and group Diffie-Hellman algorithm. (This is joint work with Paliath Narendran) 

    Language runtime systems are increasingly being embedded in systems to support runtime extensibility via mobile code. Such systems raise a number of concerns when the code running in such systems is potentially buggy or untrusted. While sophisticated access controls have been designed for mobile code and are shipping as part of commercial systems such as Java, there is no support for terminating mobile code short of terminating the entire language runtime. This paper presents a concept called ``soft termination'' which can be applied to virtually any mobile code system. Soft termination allows mobile code threads to be safely terminated while preserving the stability of the language runtime. In addition, function bodies can be permanently disabled, thwarting attacks predicated on system threads eventually calling untrusted functions. Soft termination guarantees termination by breaking any potential infinite loops in mobile code. We present a formal design for soft termination and an implementation of it for Java, built using Java bytecode rewriting, which demonstrates reasonable performance (3-25% slowdowns on benchmarks).

    In the real world, insurance is used to mitigate financial risk to individuals in many settings. Similarly, it has been suggested that insurance can be used in distributed systems, and in particular, in authentication procedures, to mitigate individual's risks there. In this talk, we further explore the use of insurance for public-key certificates and other kinds of statements. We also describe an application using threshold cryptography in which insured keys would also have an auditor involved in any transaction using the key, allowing the insurer better control over its liability. We provide a formal yet simple insurance logic that can be used to deduce the amount of insurance associated with statements based on the insurance associated with related statements. Using the logic, we show how trust relationships and insurance can work together to provide confidence.
    (This is joint work with Jon Millen, SRI International.)

    Spatial Logics Session

    Two groups have recently studied related `spatial' logics for reasoning locally about related data models: the group centering on O'Hearn and Reynolds developed a new program logic for low-level programs that manipulate RAM data structures, based on the bunched logic of O'Hearn and Pym; the group centering on Cardelli, Gardner and
    Ghelli developed techniques for analysing and manipulating  Web data (such as XML), based on the ambient logic of Cardelli and Gordon. The formal similarity of these spatial logics reflects the strong pre-formal connection between the Web and linked data structures: a URL is like an address, and a web link is like a pointer (an address embedded within a data structure).

    Gardner  will explain these connections using her recent work on querying data on the Web. This work is joint research with Luca Cardelli and Giorgio Ghelli

    We present the semantics and proof theory of a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh name quantifier. Properties of concurrent systems can also be defined by second-order quantification and hence (through an encoding) by recursion. A central aim of our logic is the combination of a logical notion of freshness with inductive and coinductive definitions of properties.

    We study the problem of decidability and validity for two spatial logics: a logic for pointers bases on the logic of Bunched Implications and a subset of the Ambient Logic. In both cases validity is undecidable in the presence of quantifiers, but the quantifier-free sublogics are decidable.

    We give a description of graphs using constructs from process algebra, which leads to a natural multiset semantics. We introduce a spatial logic for reasoning about graphs, which integrates well with our graphical models and allows us to reason locally about disjoint subgraphs  Finally, we extend our logic to provide a query language, which preserves the multiset semantics of our graph model.

    The semantics of BI, the logic of bunched implications, may be motivated by models of resource. At the most basic level, in which resources are modelled as preordered monoids, various completeness results obtain: elementary, topological and Grothendieck topological. Moving to semantic tableaux, a basis for efficient theorem proving, we obtain a complete procedure for generating models and countermodels. As a consequence we obtain for (propositional) BI the following: the finite model property, a new proof of decidability, and a completeness theorem for a resource semantics based on partial preordered monoids including, as a natural example, intuitionistic pointer logic.  

    Contributed Talks

    A reflexive domain is one that contains its own continuous function space as a retract. Reflexive domains are models of the untyped lambda calculus, and from them we build categories of partial equivalence relations, also known as PER models. The results presented in this talk were motivated by the question how many PER models on reflexive Scott domains there are, up to equivalence of categories.

    We first discuss the notion of "n-coherent" domains, a straightforward generalization of Plotkin's definition of coherently complete domains, and the related notion of a "coherence number" of a domain.

    Using results about the existence of universal n-coherent domains, we prove several domain theoretic results about reflexive domains. One such result is that a domain D is reflexive if, and only if, the product D x D is a retract of D. We also show that there are only countably many PER models on reflexive Scott domains, one for each coherence number between 1 and aleph null.

    We show how to provide an abstract, state-free semantics for a wide variety of parallel programming languages using traces. The approach is robust enough to incorporate shared-memory parallelism as well as CSP-style processes communicating synchronously, and Kahn-style networks of asynchronously communicating processes

    We begin by introducing a domain of classical states with Shannon entropy as a measurement. We then show how to construct a domain of quantum states from a domain of classical states. Moreover, the measure of content on classical states extends to a measure of content on quantum states. In the context of our example, the extension of Shannon entropy from classical to quantum states yields the fundamental von Neumann entropy. This establishes that well-known notions of information and content are instances of the measurement formalism in domain theory.

    This work opens up some striking new perspectives on fundamental issues in physics. In particular, the traditional study of the quantum structure, initiated by Birkhoff and von Neumann in terms of the lattice of projections, coincides with the study of the maximal elements of the domain of quantum states (e.g. Gleason's theorem on the measures on closed subspaces of Hilbert space). Surprisingly, by exploiting the domain theoretic structure of quantum mechanics itself (as opposed to merely representing quantum states within a domain), the domain of quantum states also naturally carries the non-unitary dynamics (collapse) of a quantum system. The is joint work with Keye Martin

    John Reynolds formalized a notion of uniformity called relational parametricity as characterized by the preservation of relations. He used this notion in giving a set-theoretic semantics of the polymorphic lambda calculus. Certain representation results for polymorphic types in the model were exhibited to show that relational parametricity captures the intuitive understanding of uniformity.

    While considering Algol-like languages, Peter O'Hearn and Bob Tennent observed that a procedure declared in some world (collection of currently allocated variables) not only runs in all future worlds, but that its behavior is uniform over all future worlds. They adapted their categorical model of Idealized Algol to include a parametricity requirement - certain relations between future worlds are preserved.This enforces some uniformity property, as they showed this model satisfied some expected program equivalence which did not hold in previous models.

    In this talk, we consider semantics for Polymorphic Algol. It seems reasonable to expect a model with two levels of parametricity requirements (that is, two different kinds of 'relations' that are preserved) corresponding to the two forms of uniformity mentioned above would satisfy both the representation results and the program equivalences. Indeed, we give such a model. However, our attempt at extending the O'Hearn-Tennent model to accommodate parametric polymorphism fails to satisfy the representation results. Analysis of what happens here points out how parametricity can improve categorical models.

    We present a specification language for first-order Algol with active expressions. The specification language has a regular-language semantic model similar to that of the programming language itself, so the validity of specifications is semantically decidable. But the specification language also enjoys good logical properties which allow composing specification by inferential reasoning. The specifications language is inspired by Reynolds's universal specifications but is based on different semantic ideas. Instead of a non-interference predicate we use a "stability" generalized universal quantifier stipulating that the object denoted by an identifier is technically well-behaved. Specifications can be verified either semantically or inferentially; we therefore argue that this specification language is suitable for compositional model checking of Algol with active expressions.

    Combining distributed parallelism and laziness requires some relaxation of the latter on behalf of the former, with the consequent introduction of speculative computation, which will range between a minimum and a maximum in each particular program execution, due to the time-dependency inherent in parallel systems. Besides, dealing with side-effects (process creation and value communication) requires to take care of the order in which expressions are evaluated.

    With these ideas in mind, we define a continuation-based denotational semantics for a very simple lazy language with explicit process creation and implicit process communication.

    There are several intersting category theoretical structures around the notion of Kleene algebra introduced by Dexter Kozen. The category of small Kleene algebras almost forms an Ab-category (only, homsets form Abelian monoids rather than Abelian groups), and this structure explains the semiring structure of Kleene algebra. This structure and the extra structure for the Kleene star allows the usual matrix presentation of finite state automata. I try to clarify these category theoretical aspects of the theory of Kleene algebra, which seems to be missing so far. I may be able to continue to my on-going work of the generalisation of Kleene algebraic approach to regular tree languages.

    Logical relations and bisimulation can be used to define when a family of labelled transition systems (LTSs) is parametric. We present a result which states that, under certain restrictions on types, a parametric family of LTSs is definable by a symbolic LTS.

    Call-by-push-value (CBPV) is a new programming language paradigm, based on the slogan ``a value is, a computation does''. We claim that CBPV provides the semantic primitives from which the call-by-value and call-by-name paradigms are built. Evidence for this claim is found in a remarkably wide range of semantics: from operational semantics, in big-step form and in machine  form, to denotational models using domains, possible worlds, continuations and games.

    In this talk, we show how, starting from a Felleisen-Friedman-style CK-machine operational semantics for CBPV, we can add control effects using an additional type constructor for outsides. We then give denotational semantics using continuations. We see that the while a value type A denotes the set of values of type A, a computation type B denotes the set of outsides for type B. We explain why, although in many models we interpret computation types by algebras for a Moggi monad, that would not be suitable in this instance.

    We see that we recover traditional continuation semantics for CBV, and Streicher-Reus' continuation semantics for CBN. We also see how to generalize our continuation semantics to model CBPV + control + other effects.

    The measurement formalism uses `domain' as a means of modelling informative objects but otherwise has goals that can safely be regarded as different from those of classical domain theory. For this reason, some may choose to say that it is a part of domain theory, while others may not. Its concern is not restricted to computer science, nor is it restricted to physics: We are interested in any discipline where the basic ideas of partiality and totality, information content, and `process' arise naturally.

    This talk is about one of the basic instruments of the measurement formalism, its informatic derivative, which offers a method for calculating the rate at which processes manipulate information with respect to a specified notion of content (measurement). Ideally, we hope to have time enough to consider examples of informatic rates of change on the interval domain, the domain of partial functions on the naturals, the domain of analytic mappings, and the domain of quantum states

    We investigate the existence of colimits in categories of ordered structures showing that topology often can be used to give an explicit representation of the colimit when it exists.

    Data refinement is the conversion of data from an interpretation in a more abstract ADT (``abstract data type'') to an interpretation in a more concrete ADT. Hoare asked when is it possible to uniquely extend a refinement from a finite specification of an ADT to the entire specification of the ADT (Hoare:1972). This is important because it is never possible to fully check a refinement of an ADT over its entire, infinite specification. Kinoshita and Power have found an elegant approach to this problem using algebraic structure and the Eilenberg-Moore category of the semantic category of the programming language concerned. However, they have not considered data refinement in a concurrent context. Indeed, little work has been done on data refinement in a concurrent context. We are working on developing a general data refinement formalism for synchronous dataflow programs, as represented by the interaction category of synchronous processes (SProc), using the Eilenberg-Moore category.

    Lax logical relations provide an alternative way of defining a refinement between extensions of SProc based on relations between sets (Plotkin:2000ppst). The advantage of lax logical relations over algebraic structure is their simplicity and their ready extensibility to alternative models of concurrency. We have applied the lax logical relations approach to refinement to both dataflow and transition systems.

    Of great interest are the insights provided by algebraic structure and lax logical relations into the meaning of data refinement for different models of concurrency, such as dataflow, transition systems, Petri nets and coloured Petri nets. Categorical interpretations of these models have much to offer in understanding data refinement in a concurrent context, especially as category theory is a convenient tool for algebraic structure and lax logical relations.

    FDR is a well-established model checker for the untimed process algebra CSP. Given two processes P and Q, FDR allows one to decide whether P is refined by Q, i.e., whether all the behaviours of Q are also possible behaviours of P. Recent work by the first author has laid a framework for extending the use of FDR to model checking Timed CSP processes. In order to apply this work to the problem of checking refinement between timed automata, one must adequately interpret timed automata within the framework of Timed CSP. Although it can be shown that no direct translation of timed automata into Timed CSP exists, we are able to provide a systematic account of how refinement between timed automata can be interpreted in Timed CSP, and thus checked on FDR. We illustrate our findings with a small case study. (This is joint work with James Worrell.)

    Recently Baier et. al. showed that if two continuous-time Markov chains (CTMSs) are bisimilar then they obey the same formulas of continuous stochastic logic (CSL). We prove that the reverse holds as well. In fact we prove this for systems where the state space may be a continuum. Along the way we give a new proof that the set of Zeno paths has measure zero if the transition rates are bounded.

    We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi's paradigm for modelling computational effects; we emphasise the importance here of the operations that induce computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi's side-effects monad transformer (an application is the combination of side-effects with nondeterminism). And We give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer (an application
    is the combination of exceptions with other effects).

    In giving a set-theoretic semantics to the polymorphic lambda calculus, John Reynolds has noted that a polymorphic type such as FORALL X. F(X) does not represent arbitrary families of elements of sets F(X), but rather only the parametric families that behave in a uniform way for all X. In his characterization, parametric families have components that preserve all possible relations between sets chosen for X. On the surface, one finds that the notion of limits in category theory is very similar to this, where LIM X. F(X) consists of families that preserve all possible morphisms between objects chosen for X.

    In this talk, we make this connection concrete by characterizing polymorphic types as form of limits (called parametric limits) in a suitable setting of categories. This enables us to generalize Reynolds's semantics to categorical level so that the ideas of polymorphism and parametricity can be interpreted in arbitrary categories with the requisite structure. We axiomatize the requisite structure so that representation results concerning polymorphic types for initial algebras and final coalgebras follow from the axioms.

    This talk gives an overview of recent work applying metric domain theory and elementary measure theory to the study of a class of reactive probabilistic transition systems -- the labelled Markov processes of Desharnais, Gupta, Jagadeesan and Panangaden. The starting point of this work is a domain equation for probabilistic bisimilarity based on the Hutchinson metric on probability measures. This yields a coinductive characterization of the metric on labelled Markov processes introduced by Desharnais et al. In turn, this suggests interesting connections between probabilistic bisimiluation on the one hand and linear programming and game theory on the other.

    We present a generalisation of the triad lts's/ (bi)simulation/Henessy-Milner logic, appropriate to directly cope with issues peculiar to processes exchanging values of arbitrary types and exhibiting imperative features. This generalisation is analysed and characterised abstractly by deploying relevant pieces of categorical machinery.

    The processes under study are categorical transition systems, transposes across the free adjunction of graph homomorphisms from a `control graph` to a category of `elementary computations' \Lb . We propose the notion of dynamic simulation which essentially allows a transition to be matched by a possibly non-trivial control path provided the labels agree. Classic strong simulation but also the classic weak one come about as special cases.

    In our abstract treatment, bimodules \ie morphisms of the bicategory \mathcal{B} of free categories and discrete fibrational spans play the r\^{o}le of generalised relations. We characterize dynamic simulation over \Lb in terms of the interaction between certain lax functors called 'modules'. This boils down to a factorisation through \Re :\, Cyl\left( \mathcal{B}\right) \rightarrow \mathcal{B}\times \mathcal{B}, the Grothendieck comprehension of the homomorphism \mathcal{B}\left( \_,\_\right) . On the logical side, we present the construction of a doctrine for a modal logic as a canonical extension of a regular fibration, here an account of the extension of a logic of `sets` and `functions` to a logic of `sets` and `bimodules`. We study its interaction with cts's and dynamic simulations and pin down the satisfaction relation over cts's as a universal dynamic simulation.

    Click here to register

    Back to MFPS 18 page