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 S=
ystems

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 L=
aird

Guy McCusker

John Power

From Imperial:

Dirk Pattinson

From Swansea:

Arnold Beckmann

Ulrich Berger

Jens Blanck

=
Fredrik Nordvall Forsberg

Roger Hindley

Karim Kanso

Andrew Lawr=
ence

Peter Mosses

Markus Roggenbach

Monika Seisenberger

Ant=
on 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.200=
9).

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 ene=
rgy management systems. Accordingly,

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

and dependabi=
lity, it however faces difficulties due to (1) increasing complexity of sys=
tem

functionality, (2) growing network scale, (3) increasing embedded d=
evices, and (4) numerous

combination of embedded environment to be cons=
idered 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 test=
ing. For this

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

referred as Company D), and Renes=
ase Technology Corp. (hereafter referred as Company R).

Both Company D =
and Company R are Japan=C2=BFs leading companies, which respectively develo=
ps

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 forma=
l model-based testing and give the outline design of a CILS

system base=
d on formal model-based testing for a real building energy management syste=
m

(BEMS) developed by Company D.

Tableau methods are one of the main techniques that underly

automate=
d reasoning for modal logics, and are implemented in an ever

growing nu=
mber of tools. Despite the fact that tableau algorithms

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

complexity bounds fo=
r the logics in question. Recently, it has been

shown that optimality c=
an 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

gl=
obal assumptions) we introduce two concrete algorithms to

decide satisf=
iability. Both algorithms are proved correct

coinductively, and can be =
seen to generalise ancestor equality

blocking, and global caching, resp=
ectively. Apart from giving a

coinductive reconstruction of ancestor eq=
uality blocking and global

caching, this showcases the wide applicabili=
ty of both and

demonstrates that automated reasoning with coalgebraic l=
ogics in the

presence of global assumptions is also in practice not (mu=
ch) harder

than for modal logics with an underlying relational semantic=
s.

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

=
a structure-respecting equivalence between the category of Lawvere

the=
ories and the category of finitary monads on **Set**. The noti=
on of

monad extends from **Set** to any base category

finitariness extends to any base cate=
gory **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 th=
e

spirit of the definition, to an arbitrary locally finitely presentabl=
e

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

categories. Moreover, we do it in a way that routi=
nely and naturally

enriches.