The fourth meeting of the Wessex Theory Seminar will take place on Thursday, 29 October in Swansea.

Lectures will be given in Robert Recorde Room (Far-205), Faraday Building, Swansea University.

Lunch and coffee will be provided.

Talks are expected to last 40 minutes, giving time for questions and change-over.

**Preliminary Programme**

1:00 Lunch

2:00--2:40: Yoshiki Kinoshita (AIST Japan): Cluster in the Loop Simulation Framework based on Formal Model-based

Testing for Embedded Network Systems

2:45--3:25: Dirk Pattinson (Imperial College): Coinduction in Proof Theory: Efficient Algorithms for Satisfiability Checking

3:30 Coffee

4:00-4:40: John Power (University of Bath): Lawvere Theories over a General Base

**Attendance**

From AIST (Japan):

Yoshiki Kinoshita

From Bath:

Ana Carolina Martins Abbud

Martin Churchill

Jim Laird

Guy McCusker

John Power

From Imperial:

Dirk Pattinson

From Swansea:

Arnold Beckmann

Ulrich Berger

Jens Blanck

Fredrik Nordvall Forsberg

Roger Hindley

Karim Kanso

Andrew Lawrence

Peter Mosses

Markus Roggenbach

Monika Seisenberger

Anton Setzer

From Southampton:

Austin Anderson

Toby Wilkinson

If you like to attend, please feel free to add your name or let me know via email:

m.seisenberger at swansea.ac.uk (Ideally by Friday 23.10.2009).

We would also like to take the opportunity to discuss/plan future Wessex Theory Seminar meetings.

After the talks we aim to go for a drink and (if your time permits) for an informal meal.

**Abstracts**

##### Yoshiki Kinoshita: Cluster in the Loop Simulation Framework based on Formal Model-based Testing for Embedded Network Systems

Embedded network systems are growing all around the world, such as in-vehicle networking

systems, consumer electronic networks and building energy management systems. Accordingly,

verification and validation of embedded network systems are important to guarantee safeness

and dependability, it however faces difficulties due to (1) increasing complexity of system

functionality, (2) growing network scale, (3) increasing embedded devices, and (4) numerous

combination of embedded environment to be considered for validation and verification. To

handle the difficulties, we plan to develop a new system to validate embedded network systems

using cluster in the loop simulation (CILS) approach and formal model-based testing. For this

purpose, we have started a collaborative project with AIST, Daikin Industries, ltd. (hereafter

referred as Company D), and Renesase Technology Corp. (hereafter referred as Company R).

Both Company D and Company R are Japan¿s leading companies, which respectively develops

air-conditioning and building energy management systems and products embedded micro

processing units and related development tools. In this paper, we explain the idea of cluster in

the loop simulation and formal model-based testing and give the outline design of a CILS

system based on formal model-based testing for a real building energy management system

(BEMS) developed by Company D.

##### Dirk Pattinson: Coinduction in Proof Theory: Efficient Algorithms for Satisfiability Checking

Tableau methods are one of the main techniques that underly

automated reasoning for modal logics, and are implemented in an ever

growing number of tools. Despite the fact that tableau algorithms

work extremely well in practice, they often do not meet the known

complexity bounds for the logics in question. Recently, it has been

shown that optimality can be obtained for some logics while

retaining practicality by using a technique called ``global caching''.

Here, we show that global caching is applicable to a wide class of modal logics,

including all those that can be equipped with coalgebraic semantics.

Starting from a sound and complete tableau calculus (and a set of

global assumptions) we introduce two concrete algorithms to

decide satisfiability. Both algorithms are proved correct

coinductively, and can be seen to generalise ancestor equality

blocking, and global caching, respectively. Apart from giving a

coinductive reconstruction of ancestor equality blocking and global

caching, this showcases the wide applicability of both and

demonstrates that automated reasoning with coalgebraic logics in the

presence of global assumptions is also in practice not (much) harder

than for modal logics with an underlying relational semantics.

##### John Power: Lawvere Theories over a General Base

The notion of Lawvere theory can be characterised by the presence of

a structure-respecting equivalence between the category of Lawvere

theories and the category of finitary monads on **Set**. The notion of

monad extends from **Set** to any base category **C**, and the notion of

finitariness extends to any base category **C** that is locally finitely

presentable. Moreover, this all enriches. But what about the notion of

Lawvere theory?

In this talk, we extend the notion of Lawvere theory, while retaining the

spirit of the definition, to an arbitrary locally finitely presentable

base category **C** in a way that naturally extends the above equivalence of

categories. Moreover, we do it in a way that routinely and naturally

enriches.