% abstracts.txt -*- text -*- % Version of 03 October 2009, 08:00 ---------- TITLE: A Singular Choice for Multiple Choice SPEAKER: Gudmund S. Frandsen Aarhus University ABSTRACT: How should multiple choice tests be scored and graded, in particular when students are allowed to check several boxes to convey partial knowledge? Many strategies may seem reasonable, but we demonstrate that five self-evident axioms are sufficient to determine completely the correct strategy. We also discuss how to measure robustness of the obtained grades. Our results have practical advantages and also suggest criteria for designing multiple choice questions. Joint work with Michael I. Schwartzbach. ---------- TITLE: Exponential decay in probabilistic trust models SPEAKER: Vladimiro Sassone University of Southampton ABSTRACT: Research in models for experience-based trust management has either ignored the problem of modelling and reasoning about dynamically changing principal behaviour, or provided ad-hoc solutions to it. Using Hidden Markov Models to represent principal behaviours, we focus on computational trust frameworks based on the `beta' probability distribution and the principle of exponential decay, and derive a analytical formula for the estimation error they induce. This allows potential adopters of beta-based computational trust frameworks and algorithms to better understand the implications of their choice. ---------- TITLE: Primes, presheaves and (co)reflections SPEAKER: Glynn Winskel Cambridge University: ---------- TITLE: Probabilistic Approximations of Signaling Pathways Dynamics SPEAKER: P.S. Thiagarajan School of Computing, National University of Singapore ABSTRACT: A standard formalism used to model signaling pathways dynamics is a system of Ordinary Differential Equations (ODEs). Signaling pathways usually involve a large number of molecular species and bio-chemical reactions. Hence the corresponding system of ODEs will not yield closed form solutions. In fact, they are difficult to study even via numerical solutions. To deal with this, we propose a probabilistic approximation technique which consists of first sampling a representative set of trajectories and then exploiting the structure of the pathway to encode these trajectories compactly as a Bayesian network (BN). As a result, many interesting dynamic properties can be analyzed efficiently through standard Bayesian inference techniques, instead of resorting to a large scale ODE simulations. Our preliminary results are promising in terms of both accuracy and efficiency. ---------- TITLE: What is a process? SPEAKER: Robin Milner University of Cambridge and University of Edinburgh ABSTRACT: In 1978 I thought it might take perhaps 3 months to define what a process is, analogous to the definition of a function as a set of ordered pairs. After 3 decades the question remains open. It seems there are many definitions, and we have to be clear how our definition should treat causality, the structure of non-deterministic choices, the nature of interactions, and probabilities. So I'll give just one answer, almost exactly the one I began with in '78, but giving all the rationale for it. Other valid answers have rationale too. I also want to pay credit to Mogens for the discussions we had at that time, and for his important work later that led us to the pi calculus. ---------- TITLE: Applied Proof Theory SPEAKER: Ulrich Kohlenbach Department of Mathematics, Technische Universität Darmstadt ABSTRACT: During the last 15-20 years an applied form of proof theory emerged which is concerned with the extraction of computational and combinatorial content from proofs. This has led to applications in computer science and different areas of mathematics. We will give a survey on some of these developments. ---------- TITLE: On Bisimulation and Modularity SPEAKER: Peter D. Mosses Swansea University ABSTRACT: We are investigating the modularity of transition system specifications in SOS. Our aim is a rule format, together with a definition of bisimulation, such that equations between open terms are robust under disjoint extension; we discuss some possibilities. Analogous results for MSOS specifications would provide a further degree of modularity, since MSOS rules never need to be reformulated when the specified language is extended. Joint work with MohammadReza Mousavi and Michel Reniers (TU Eindhoven) ---------- TITLE: The wire calculus SPEAKER: Pawel Sobocinski University of Southampton ABSTRACT: The wire calculus is a process algebra for modelling truly concurrent systems with explicit network topologies. Instead of a Dijsktra-Hoare-Milner commutative parallel operator it features a non-communicating non-commutative parallel and an operator for synchronisation on a common boundary. The dynamics are handled by operators inspired by Milner's CCS and Hoare's CSP: unary prefix operation, binary choice and a standard recursion construct. The operational semantics is a labelled transition systems derived using SOS rules. After presenting the formal definition of the calculus I will discuss some basic results and give several examples. ---------- TITLE: Characteristic Formulae for Fixed-Point Semantics: A General Framework SPEAKER: Luca Aceto Reykjavík University ABSTRACT: The literature on concurrency theory offers a wealth of examples of characteristic-formula constructions for various behavioural relations over finite labelled transition systems and Kripke structures that are defined in terms of fixed points of suitable functions. Such constructions and their proofs of correctness have been developed independently, but have a common underlying structure. In this talk I will present a general view of characteristic formulae that are expressed in terms of logics with a facility for the recursive definition of formulae. I will show how several examples of characteristic-formula constructions from the literature can be recovered as instances of the proposed general framework, and how the framework can be used to yield novel constructions. Joint work with Anna Ingólfsdóttir and Joshua Sack, Reykjavík University ---------- TITLE: Interactive Configuration Problems SPEAKER: Henrik Reif Andersen Configit A/S, Copenhagen ABSTRACT: In the talk, I will link the math of constraint satisfaction problems to guiding user interfaces and explain how we are using this in Configit. It covers several papers on the issue we have written over the years. I will also include some stories on how this relates back to the classes I was taught by Mogens and how this influenced my future. ---------- TITLE: Specifying Interacting Components with Coordinated Concurrent Scenarios SPEAKER: Madhavan Mukund Chennai Mathematical Institute ABSTRACT: We introduce a visual notation for local specification of concurrent components based on message sequence charts (MSCs). Each component is a finite-state machine whose actions are MSCs that specify its local view of the overall communication in the system. These local MSCs are composed into coherent global scenarios using a separately specified set of transactions. Intuitively, each MSC represents a phase of interaction. We introduce a mechanism to overlap phases that allows complex interactions to be specified without obscuring the logical structure of the constituent scenarios. Our notation combines the global view available in models such as high-level message sequence charts (HMSCs) with the local, asynchronous structure captured by message-passing automata (MPA). In this talk we focus on the syntax and formal semantics of our notation, with examples that illustrate why this approach is more natural for capturing real-life specifications. Joint work with Prakash Chandrasekaran. ---------- TITLE: Efficient Symbolic Execution Algorithms for Programs Manipulating Dynamic Heap Objects and Contracts SPEAKER: Jooyong Lee Kansas State University ABSTRACT: Modern software systems often use object-oriented programs that dynamically create and manipulate objects. Such programs are difficult to analyze due to issues such as aliasing. We have developed a fully automatic analysis method to check functional correctness of such programs. The approach extends the classical symbolic execution algorithm with a graphical representation of the heap. I will explain what extension we made, and optimizations we made to this extension. As to functional correctness, we expect it to be expressed in JML (Java Modeling Language) while possible exceptions are still checked even when no correctness specification is given. I will explain how we could incorporate JML expressions into our symbolic-execution framework. Joint work with Robby and Xianghua Deng. ---------- TITLE: The Role of Trust in Computer Security SPEAKER: Christian Damsgaard Jensen Technical University of Denmark ---------- TITLE: Exponential Decay in Probabilistic Trust Models SPEAKER: Vladimiro Sassone University of Southampton ABSTRACT: Research in models for experience-based trust management has either ignored the problem of modelling and reasoning about dynamically changing principal behaviour, or provided ad-hoc solutions to it. Using Hidden Markov Models to represent principal behaviours, we focus on computational trust frameworks based on the `beta' probability distribution and the principle of exponential decay, and derive a analytical formula for the estimation error they induce. This allows potential adopters of beta-based computational trust frameworks and algorithms to better understand the implications of their choice. ---------- TITLE: Model-checking Games for Fixpoint Logics with Partial Order Models SPEAKER: Julian Bradfield University of Edinburgh ABSTRACT: We introduce model-checking games that allow \emph{local} second-order power on \emph{sets} of independent transitions in the underlying partial order models where the games are played. Since the one-step interleaving semantics of such models is not considered, some problems that may arise when using interleaving semantics are avoided and new decidability results for partial orders are achieved. The games are shown to be \emph{sound} and \emph{complete}, and therefore determined. While in the interleaving case they coincide with the local model-checking games for the $\mu$-calculus, $L\mu$, in a noninterleaving setting they verify properties of Separation Fixpoint Logic (SFL), a logic that can specify in partial orders properties not expressible with $L\mu$. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving previous results in the literature. Joint with Julian Gutierrez, LFCS, University of Edinburgh. ---------- TITLE: On Determinism in Modal Transition Systems SPEAKERS: Nikola Benes and Jan Kretinsky, Masaryk University, Brno Kim G. Larsen and Jiri Srba, Aalborg University ABSTRACT: Modal transition systems (MTS) is a formalism which extends the classical notion of labelled transition systems by introducing transitions of two types: must transitions that have to be present in any implementation of the MTS and may transitions that are allowed but not required. The MTS framework has proved to be useful as a specification formalism of component-based systems as it supports compositional verification and stepwise refinement. Nevertheless, there are some limitations of the theory, namely that the naturally defined notions of modal refinement and modal composition are incomplete with respect to the semantic view based on the sets of the implementations of a given MTS specification. Recent work indicates that some of these limitations might be overcome by considering deterministic systems, which seem to be more manageable but still interesting for several application areas. In the present article, we provide a comprehensive account of the MTS framework in the deterministic setting. We study a number of problems previously considered on MTS and point out to what extend we can expect better results under the restriction of determinism. ---------- TITLE: Extended Computation Tree Logic SPEAKER: Martin Lange University of Munich ABSTRACT: We introduce a generic extension of the standard computation tree logic CTL in which the Until operator is parametrized by a formal language of finite words constraining the moments along a path at which this until may be fulfilled. We briefly motivate the use of such logics and then focus on decidability and complexity results for the satisfiability and model checking problems, and on expressive power of these logics. Joint work in progress with Roland Axelsson and Markus Latte of the University of Munich and Matthew Hague and Stephan Kreutzer of Oxford University. ---------- TITLE: SPEAKER: Mogens Nielsen AArhus University ---------- end of abstracts.txt