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.