Neighbourhood semantics forms a generalisation of Kripke semantics, and it has become the standard tool for reasoning about non-normal modal logics in which (Kripke valid) principles such as []p /\ []q (Meet) and []p -> (Mon) are considered not to hold. In computer science and social choice theory, non-normal modal logics are …
read moreBooking Holidays with Linear Logic
I will present ideas for a new coordination language based on Intuitionistic Temporal Linear Logic (ITLL), extending my earlier presentation on the encoding of Reo synchronous steps into Linear Logic. This time I will show that ITLL is expressive enough to encode the (comprehensible) part of Reo. To demonstrate this …
read moreFormal languages and computable semantics for continuous mathematics
In this talk I will first outline Weihrauch's computable analysis, which gives a framework for discussing computability in topology, geometry and analysis based on type-two recursive function theory. I will then discuss some possibilities for a formal language for computable continuous mathematics. Ideally, such a language should be expressive enough …
read moreWeb Services Choreography and Orchestration in Reo and Constraint Automata
Currently web services constitute one of the most important topics in the realm of the World Wide Web. Composition of web services lets developers create applications on top of service-oriented computing platforms. Current web services choreography and orchestration proposals, such as BPEL4WS, WSCDL, and WSCI, provide notations for describing the …
read more2APL: A Practical Agent Programming Language
In this talk, I will give a brief overview of agent-oriented software development followed by the presentation of (the syntax and semantics of) an agent-oriented programming language, called 2APL (A Practical Agent Programming Language). This programming language facilitates the implementation of multi-agent systems consisting of individual cognitive agents that are …
read moreVerification of Rebeca models using symmetry and partial order reduction techniques
Rebeca is an actor-based language with formal semantics that can be used at a high level of abstraction in modeling concurrent and distributed reactive systems. The asynchronous message-passing paradigm in Rebeca allows for efficient modeling of loosely-coupled distributed systems. The simple Java-like syntax of Rebeca, unlike the traditional notations of …
read moreKeeping Secrets in Resource Aware Components
This talk will describe one of the analysis tools that we have been developing for the Trust4all project. It is an extension of the work on Q-automata that has previously been at an AGC talk. Members of SEN2 have helped implement some of this work in mCRL.
We present a …
read moreBehaviour-aware aggregation and adaptation of Web services
Service-oriented computing is emerging as a new promising computing paradigm, that centers on the notion of service as the basic element for developing future distributed heterogeneous software applications.
The ability to aggregate separate services can allow a business entity to interact with a variety of service providers to re-brand, host …
read moreComponent connectors with QoS Guarantees
Recently, it is realized that in distributed applications, software engineers must also consider Quality of Service (QoS), which is a measure of the non-functional properties of services along multiple dimensions, such as reliability, security, scalability, performance (response time, for instance), etc. when designing component connections. In this talk we will …
read moreBehavioural differential equations and coinduction for binary trees
A binary tree T can be encoded as a function from the set of words over the alphabet {0,1} to a set K (corresponding to the information stored in the nodes). If this set K has a semiring structure then T is a formal power series. Following previous work …
read more