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

=20Lectures will be given in Robert Recorde Room (Far-205), Faraday Buildin= g, Swansea University.

=20Lunch and coffee will be provided.

=20Talks are expected to last 40 minutes, giving time for questions and cha=
nge-over.

1:00 Lunch

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

Testing for Embedded Network=
Systems

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

=203:30 Coffee

=204:00-4:40: John Power (University of Bath): Lawvere Theories over a Gene= ral Base

=20From AIST (Japan):

Yoshiki Kinoshita

From Bath:

Ana Carolina Martins Abbud

Martin Churchill

=
Jim Laird

Guy McCusker

John Power

From Imperial:

Dirk Pattinson

<=
/p>=20

From Swansea:

Arnold Beckmann

Ulrich Berger

Jens Blanc=
k

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.2=
009).

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

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

=20Embedded network systems are growing all around the world, such as in-ve=
hicle networking

systems, consumer electronic networks and building e=
nergy management systems. Accordingly,

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

and dep=
endability, it however faces difficulties due to (1) increasing complexity =
of system

functionality, (2) growing network scale, (3) increasing em=
bedded devices, and (4) numerous

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

handle the diffi=
culties, we plan to develop a new system to validate embedded network syste=
ms

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

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

referred as Com=
pany D), and Renesase Technology Corp. (hereafter referred as Company R).** Both Company D and Company R are Japan¿s leading companies, whi=
ch respectively develops air-conditioning and building energy managem=
ent systems and products embedded micro processing units and related =
development tools. In this paper, we explain the idea of cluster in t=
he loop simulation and formal model-based testing and give the outline desi=
gn of a CILS system based on formal model-based testing for a real bu=
ilding energy management system (BEMS) developed by Company D.**

Tableau methods are one of the main techniques that underly

automa=
ted reasoning for modal logics, and are implemented in an ever

growin=
g number of tools. Despite the fact that tableau algorithms

work extr=
emely well in practice, they often do not meet the known

complexity b=
ounds for the logics in question. Recently, it has been

shown that op=
timality can be obtained for some logics while

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

Here, we show that g=
lobal caching is applicable to a wide class of modal logics,

includin=
g 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 sa=
tisfiability. Both algorithms are proved correct

coinductively, and c=
an be seen to generalise ancestor equality

blocking, and global cachi=
ng, respectively. Apart from giving a

coinductive reconstruction of a=
ncestor 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 r=
elational semantics.

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 categor=
y **C**, and the notion of

finitariness extends to any b=
ase category **C** that is locally finitely

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

Lawvere th=
eory?

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

spirit of the definition, to an arbitrary locally finitely presenta=
ble

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.