Loco Lunch

Spring 2012

14th June	Amir Niknafs Kermani	TBA	TBA
21st June	Michel Ludwig	TBA	TBA
(Postponed until the Autumn)	Vladimir Sazonov	On naturally continuous non-dcpo domains	After works of Normann and the author on sequentially computable finite type functionals [11], [12], [16], the necessity and possibility of a non-dcpo (non-directly complete partial ordered) domain theory became evident. In this talk, the category of continuous dcpo domains is generalized to a category of ‘naturally’ continuous non-dcpo domains with ‘naturally’ continuous maps as arrows. A full subcategory of the latter, assuming a kind of bounded completeness requirement of domains and presence of `undefined' element in each, proves to be Cartesian closed and equivalent to a subclass of Ershov’s general A-spaces. This extends a non-dcpo generalization of Scott (algebraic) domains introduced and proved to be equivalent to Ershov’s general f-spaces in recent works by the author [16], [17]. References [11] D. Normann, On sequential functionals of type 3, Mathematical Structures in Computer Science, 16 (2) (2006) 279–289. [12] D. Normann, V. Yu. Sazonov, The extensional ordering of the sequential functionals, Annals of Pure and Applied Logic, (2012), pp. 575-603 doi:10.1016/j.apal.2011.06.013, Available online 20 July 2011. [16] V. Sazonov, Inductive Definition and Domain Theoretic Properties of Fully Abstract Models for PCF and PCF+, Logical Methods in Computer Science, 3 (3:7) (2007) 1–50. http://www.lmcs-online.org. [17] V. Sazonov, Natural non-dcpo domains and f-spaces, Annals of Pure and Applied Logic 159 (2009) 341–355.

Previous Talks

Winter 2012

January 12th	Clare Dixon	Towards Temporal Verification of Emergent Behaviours in Swarm Robotic Systems	A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on: the simplicity of the individual robots; the fault tolerance inherent in having a large population of often identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms are being deployed in increasingly sophisticated areas, designing individual control algorithms that can guarantee the required global behaviour is difficult. In this talk we apply and assess the use of formal verification techniques, , in particular that of model checking, for analysing the emergent behaviours of robotic swarms. We target a particular swarm control algorithm, and show how automated temporal analysis can help to refine and analyse such an algorithm.
January 19th	Arnaud Sangnier	Parameterized Verification of Ad Hoc Networks	We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with selective broadcast. The communication topology of a network is represented as a graph. Nodes represent states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via selective broadcast messages. Reception of a broadcast is restricted to single-hop neighbors. For this model we consider verification problems that can be expressed as reachability of configurations with one node (resp. all nodes) in a certain state from an initial configuration with an arbitrary number of nodes and unknown topology. We are interested in decision problems that are parametric on the size and on the shape of the communication topology of the initial configurations. We draw a complete picture of the decidability boundaries of these problems according to different assumptions on the mobility of the nodes in the networks and on the form of the communication graphs. This is a joint work with Giorgio Delzanno (University of Genova) and Gianluigi Zavattaro (University of Bologna).
February 9th	Abdulbasit Ahmed		Intrusion Detection Systems (IDS) aim to detect the actions that attempt to compromise the confidentiality, availability, and integrity of a resource by monitoring the events occurring in computer systems and/or networks. Stream data processing is a database technology applied to flows of data. Temporal Logic is a formalism for representing change over time. This paper proposes the development of a network intrusion detection system by combining temporal formalisms for representing attack patterns with stream processing for intruder detection. The experimental results show that this combination successfully was able to detect all the attacks of that type in the test data. Additionally, the solution provides a concise and unambiguous way to formally represent attack signatures and it is extensible and scalable.
March 1st	Michael Fisher		I will talk about two things neither of which are technical: our new "Reconfigurable Autonomy" EPSRC project which will start on 30th March (Louise will be the RA); the new "Centre for Autonomous Systems Technology" that we are proposing within the University.
March 15th	ARW 5 Minute Talks
March 22nd	Louise Dennis	Verifying Reasoning within Agent-based Hybrid Control Systems

Autumn 2011

October 6th	Mark Reynolds	A Tableau for CTL*
October 13th	Frank Wolter	Ontology-Based Data Access and Constraint Satisfaction	In recent years, the use of ontologies (=logical theories) to access instance data has become increasingly popular. The general idea is that an ontology provides a vocabulary or conceptual model for the application domain, which can then be used as an interface for querying instance data and to derive additional facts. In this presentation, I will introduce ontology-based data access for ontologies given in description logics and investigate the following non-uniform complexity problem: what is the data complexity of query answering for a fixed ontology? We determine large and natural classes of ontologies for which non-uniform data-complexity of query answering is in P and even AC0. Then we show that for the basic description logic ALC, this problem is equivalent to the non-uniform complexity problem for constraint satisfaction with finite templates. Examples of consequences include: (i) a P/NP dichotomy holds for ontology based data access with ALC if, and only if, Feder and Vardi's dichotomy conjecture holds; (ii) results on first-order constraint satisfaction problems by Larose et al. correspond exactly to reductions of ontology based data access with ALC to standard queryanswering over relational databases.
October 20th	Louise Dennis	Plan Indexing for State-based Plans	We consider the issue of indexing plans (or rules) in the implementation of BDI languages. In particular we look at the issue of plans which are not triggered by the occurence of specific events. The selection of a plan from such a set represents one of the major bottle-necks in the execution of BDI programs. This bottle-neck is particularly obvious when attempting to use program model checkers to reason about such languages. I will describe the problem and examine one possible indexing scheme. I evaluate the scheme experimentally and concludes that it is only of benefit in fairly specific circumstances. I then discusses ways the indexing mechanism could be improved to provide wider benefits.
November 10th	Martin Dieguez Lodeiro	Temporal Answer Set Programming	Answer Set Programming (ASP) has emerged in the recent years as a powerful paradigm for declarative problem solving, which has its roots in knowledge representation and non-monotonic logic programming. Similar to SAT solving, the basic idea is to encode solutions to a problem in the models of a non-monotonic program. This program can be computed by reasoning engines off the shelf, dealing with the use of this paradigm to many diferent types of scenarios. The main problem that ASP presents in the representation of temporal scenarios is that time has to be reified using variables with finite domains, therefore we cannot prove the non-existence of plans or check temporal properties over temporal systems. To overcome these limitations, several extensions and formalisms that extend the syntax with temporal operators has been developed.
November 24th	John Fearnley

Spring 2011

May 18th	Vladimir Sazonov	On the extensional ordering of the sequential functionals	A joint work with Dag Normann, Oslo. The paper to appear in APAL. Abstract We will discuss the nature of the extensional ordering on the structure Q_σ of the hereditarily sequential functionals of finite types. It was shown by Dag Normann (MFCS 2006) that it is non-dcpo - a kind of anomaly. On the other hand, it still has good domain theoretical properties if to use so called natural domains (V. Sazonov, LMCS 2007, APAL 2009) as generalised Scott domains. In the current work we characterise the anomalies of Q_&sigma from the traditional domain theoretic point of view with a focus on: when the sequential functionals of a given type form a directed complete partial ordering (dcpo), and when a finite sequential functional is the nontrivial least upper bound of an infinite chain of sequential functionals.
June 1st	Yoshihito Tanaka	Conservativity of Boolean algebras with operators over semilattices with operators (joint work with Agi Kurucz, Frank Wolter and Michael Zakharyaschev)	The problems considered in this paper originate in recent applications of large scale ontologies in medicine and other life sciences. The profile OWL2EL of the OWL2 Web Ontology Language, used for this purpose, is based on the description logic EL. The syntactic terms of EL, called concepts, are interpreted as sets in first-order relational models. From a modal logic point of view, concepts are modal formulas constructed from propositional variables and the constants top, bottom using conjunction and diamonds. An EL-theory is a set of inclusions (or implications) between such concepts, and the main reasoning problem in applications of EL in life sciences is to decide whether an EL-theory entails a concept inclusion when interpreted over a class of relational structures satisfying certain constraints on its binary relations. Standard constraints in OWL2EL are transitivity and reflexivity, for which reasoning in EL is PTime-complete, as well as symmetry and functionality, for which reasoning is ExpTime-complete. As in modal logic, apart from reasoning over relational models, one can try to develop a purely syntactical reasoning machinery using a calculus. In other words, we can define a more general algebraic semantics for EL: the underlying algebras are bounded meet-semilattices with monotone operators (SLOs, for short), constraints are given by equational theories of SLOs, and the reasoning problem is validity of quasi-equations in such equational theories. The resulting more general entailment problem is not necessarily complete with respect to the `intended' relational semantics. This paper presents our initial results in an attempt to clarify which equational theories of SLOs are complete in this sense and which are not. We also prove that the completeness problem---given a finitely axiomatised equational theory of SLOs, decide whether it is complete with respect to the relational semantics---is algorithmically undecidable, which establishes a principle limitation regarding possible answers to our research question.
June 9th	Sven Schewe	Sex, Crime, and the Complexity of Minimising Deterministic Büchi, Co-Büchi, and Parity Automata	As it happens, I have never given a talk about any of the three topics, so I will focus on the most exciting among them: the third. Omega automata occur sometimes in model checking and usually in synthesis, so a minimisation procedure would be nice to have. But can we? Is it tractable? Yes we can has become a proverb, but in this case we will establish the NP completeness of this problem (or, more precise, the related decision problem). As problems do not go away only because they are intractable, we also discuss tractable techniques to reduce the state-space of Büchi automata.
June 16th	Alexei Lisitsa	Unreasonable efficiency of finite model finding in verification.	In this talk I will discuss the recent developments in FCM (finite countermodels) verification approach to parameterized verification. A few case studies will be presented and relative completeness of the method with respect to the following will be either discussed or mentioned: monotonic abstraction and symbolic reachability methods; regular model checking; regular tree model checking; tree automata completion techniques.
June 30th	Thomas Praveen Methrayil Varghese	Determinising omega automata with strong fairness acceptance conditions	Omega automata are finite automata reading infinite objects. They are of practical use in the formal analysis of reactive systems. These automata differ in their transition function (alternating, non-deterministic, universal, and deterministic) and acceptance condition (Safety, Büchi, Rabin, Muller, Streett, parity, etc.). We consider a class of omega automata with acceptance condition relating to strong fairness -- Streett automata. We take a look at some recent results with respect to the determinisation of Streett automata.
June 30th	Richard Stocker	A Formal Semantics for Brahms
July 28th	Michel Ludwig	Conjunctive Query Inseparability of OWL 2QL TBoxes	The OWL 2 profile profile OWL 2 QL, based on the DL-Lite family of description logics, is emerging as a major language for developing new ontologies and approximating the existing ones. Its main application is ontology-based data access, where ontologies are used to provide background knowledge for answering queries over data. In this talk we present recent results regarding the complexity of deciding conjunctive query inseparability for OWL 2 QL ontologies. We also demonstrate with results obtained from experiments that polynomial time (incomplete) algorithms can be used for practical module extraction.

Winter 2011

January 27th	Michael Fisher	Flight Certification for Autonomous Unmanned Aircraft?	joint work with: Matt Webster [Virtual Engineering Centre, Daresbury] Neil Cameron [Virtual Engineering Centre, Daresbury] Mike Jump [School of Engineering, Univ. Liverpool] ABSTRACT: Unmanned Aircraft are currently not allowed to fly autonomously in UK civil airpsace. Currently, there is no specific mechanism for certifying that such autonomous air systems are safe. But, what is the difference between an autonomous unmanned aircraft and the same aircraft with a pilot in? Clearly, one has a software controller (typically, an "agent") while the other has a pilot. But, for a pilot to be allowed to control an aircraft (s)he must have passed a test relating to the "Rules of the Air". Why can't we do the same with the autonomous agent? We are trying to show, for a small number of flight rules (from the "Rules of the Air"), that the autonomous agent controlling the aircraft will obey these rules and so will do what a pilot would do in its place. And we are trying to show this using formal verification. In this paper I will give an outline of our approach.
February 10th	Ullrich Hustadt	A Comparison of Solvers for Propositional Dynamic Logic	Decision procedures for propositional dynamic logics have been investigated since the introduction of this logic in the late seventies. Only in recent years have practical procedures been suggested and implemented. In this talk I will give a general overview of dynamic logic itself and describe key aspects of decision procedures for the satisfiability problem in dynamic logic. The focus of the talk will be on approaches to the construction of benchmarking formulae for the evaluation of implemented decision procedures. The benchmarking approach presented in the talk is not specific to dynamic logics, but is intended to be a general methodology for the evaluation of solvers for non-classical logics. As a case study I will then present results of such an evaluation for the current generation of implemented decision procedures for propositional dynamic logic, namely, the Tableau Workbench by Abate, Gore, and Widmann (2009), the pdlProver system by Gore and Widmann (2009), and the MLSolver system by Friedmann and Lange (2009).
March 2nd	Grant Malcolm	Algebraic Specification of Systems of Concurrent Components	We give an overview of recent work in component-based approaches to system specification, and suggest how this might extend to dynamic systems (i.e., systems whose architecture changes over time).
March 23rd	Yoshihito Tanaka	Infinitary operators in modal logics	First, we present cut-elimination theorems for infinitary modal logic and common knowledge logic. Secondly, we give a representation of modal algebras which preserves certain meets and joins, and show the completeness theorems for some classes of infinitary modal logics and non-compact modal logics. Lastly, we present a canonical formula for Heyting algebras.

Autumn 2010

September 30th	Robert Piro
October 7th	Clare Dixon	CTL-Like Fragments of a Temporal Logic of Robustness	The logic RoCTL* is an extension of the branching time temporal logic CTL* to represent robustness of systems to transient failures such as loss of data packets. New operators are introduced dealing with obligation (where no failures occur) and robustness (where at most one additional failure occurs). The only known decision procedures for the temporal logic of robustness RoCTL* are non-elementary. Here we propose two CTL-like restrictions of RoCTL, Pair-RoCTL and State-RoCTL. We investigate whether it is possible to translate these fragments into CTL showing whilst this is not in general possible for Pair-RoCTL it is for State-RoCTL. We obtain a satisfiability preserving translation for State-RoCTL into CTL showing that the complexity of satisfiability of State-RoCTL is EXPTIME-complete. We also show that these fragments of RoCTL are useful in specifying systems.
October 21st	Richard Stocker	Towards the Verification of Human-Agent Teamwork	Looking towards the development of tools capable of automatically analysing human-agent teamwork. Specifically, to analyse the Brahms modelling framework, together with abstraction into agent code, and application of automated agent verification techniques (such as model checking) for agent programs in order to analyse human-agent collaborative activities modelled by Brahms.
October 28th	Rafiq Saleh	Planarity of knots by automata and logic	We investigate the descriptional complexity of knot problems and show lower and upper bounds for the planarity problem of knot diagrams represented by Gauss words. We study these problems in the context of automata models over an infinite alphabet and by their expressibility in first order logic and its extensions.
November 18th	Savas Konur	Analyzing Robot Swarm Behaviour using Probabilistic Model Checking	An alternative to deploying a robot of high complexity can be to utilize robot swarms comprising large numbers of identical, and simple, robots. Such swarms have been shown to be adaptable, fault-tolerant and widely applicable. However, designing individual robot algorithms to ensure effective and correct swarm behaviour is actually very difficult. While mechanisms for assessing the effectiveness of any swarm algorithm before deployment are essential, such mechanisms have traditionally involved computational simulations of swarm behaviour, but such simulations do not involve a deep analysis of all possible swarm behaviours. So, in this paper, we will develop the use of automated formal verification techniques, involving an exhaustive mathematical analysis, in order to assess whether swarms will indeed behave as required.
December 2nd	Abdulbasit Ahmed		Intrusion Detection Systems (IDS) aim to detect the actions that attempt to compromise the confidentiality, availability, and integrity of a resource by monitoring the events occurring in computer systems and/or networks. Stream data processing is a database technology applied to flows of data. Temporal Logic is a formalism for representing change over time. We propose the development of an intrusion detection system by combining temporal formalisms for representing attack patterns with stream processing for intruder detections. The experimental results show that this combination successfully was able to detect all the intrusions or attacks in the test data. Additionally, the solution provides a concise and unambiguous way to formally represent attack signatures and it is extensible and scalable.
December 8th	Everyone	Loco Christmas Lunch	Bring Sweet things to share.

Spring 2010

May 27th

Sherly Nietiadi

Tableau Algorithm for Temporal Logic with Constraints

Often when formalising dynamic systems, constraints such as exactly "n" of a set of values hold. In this talk, we consider reasoning about propositional linear time temporal logics in the presence of such constraints. We discuss BeTL, an implemented prover temporal logics with constraints using a tableau-like algorithm, which shows the advantages of incorporating constraints into temporal reasoning.

However, BeTL has a number of drawbacks including explicitly evaluating the constraints, the need for input in a particular normal form and an expensive breadth-first style of construction. To address this, we provide a (more standard) temporal tableau algorithm, incorporating constraints, which is sound, complete and terminating.