There is an obvious connection between coalgebra and modal logic: Coalgebras for an endofunctor T can be seen as abstract dynamic systems or transition systems, and modal logic seems to be the natural specification language to talk about these systems. Monotone modal logics generalise normal modal logics by weakening the …
read moreThe Differential Calculus of Bitstreams
Using (stream) differential equations for definitions and coinduction for proofs, we define, analyse, and relate in a uniform way four different algebraic structures on the set of bitstreams (infinite sequences of 0's and 1's), characterising them in terms of the digital circuits they can describe.
read moreReo: Operational Semantics, Animation and Model Checking
In this talk, we first present an operational semantics for Reo in the style of Plotkin's SOS (Structured Operational Semantics). Next, we present a faithful translation of this semantics into Maude (a conditional term rewriting language). This, in turn, allows us to benefit from the tooling around Maude in order …
read moreMOnitoring Distributed Object and Component Communication
"Monitoring of the behavior of computer programs enjoys applications in activities such as debugging, testing, and software management. For example, in debugging, developers use information collected during application runtime to pinpoint the source(s) of application behavior they consider erroneous. On this talk I present my work on monitoring communication …
read moreReo: Semantics and Tools for Design and Analysis. State-of-the-Art and Future Work
Reo is a channel-based exogenous coordination model wherein complex coordinators are compositionally built out of basic channel types (like synchronous or FIFO channels) and connectors. In this talk, first we will briefly explain the semantics of Reo based on languages of Timed Data Streams and an operational semantics based on …
read moreStone Coalgebras and Completeness for Coalgebraic Modal Logic
Coalgebras have been studied as a general approach to dynamic systems. Modal logic seems to be a natural choice for a specification language for coalgebras. Given an endofuntor T the problem is how to define a suitable modal logic for T-coalgebras. Following an approach by Pattinson we first define for …
read moreNormative Multiagent Systems
In a previous ACG presentation earlier this year I have discussed the basics of input/output logics (iol), which I developed together with David Makinson from King's College London. In this talk I discuss how a rule based logic like iol can be used in agent architectures, as well as …
read moreA Comparative Study of Arithmetic Constraints on Integer Intervals
The subject of arithmetic constraints on reals has attracted a great deal of attention in the literature. For some reason arithmetic constraints on integers have not been studied, even though they are supported in a number of constraint programming systems. In this presentation we will discuss various alternative approaches, based …
read moreIntegrating Formal Methods with XML
Stating formalisms in XML adds the interoperability benefit of XML to them. Existing tools for formal methods are based on a particular implementation of the semantics of the computational model in a tool-specific format. This complicates interoperability. Instead we propose to use XML also for representing the semantics and even …
read moreVerification of Security Protocols with Rebeca
The correctness of security protocols has become more and more important lately, as the aspects of real life being in control of computer systems increased. As operations like money transfers or military communications are being ported to computer networks, any flaw in security of the systems can lead to extremely …
read more