KTH / CSC / TCS

Logic and Semantics Group

The logic and semantics group organize meetings where students and tutors present and discuss topics related to logics and semantics.

Forthcoming meetings in reverse chronological order

Thursday, 25th of March, 15:00, Room 1537:
Quantitative Model Checking (Musard Balliu)

In this talk I will present some advances in the area of quantitative model checking (QMC). QMC concerns the formal verification quantitative properties of automated systems such as probabilistic, real time and hybrid systems. In particular, I will concentrate on explicit state model checking and probabilistic model checking and discuss problems, solutions and tools used in the current state of art of this area.

Wednesday, 30th of September, 10:30, Room 1535:
Generating a Model of a Communication Protocol from Test Data (Siavash Soleimanifard)

Model-based techniques for verification and validation require a model of the system under test (SUT). However, most communication systems lack a complete, correct model. One approach for generating a model of a system is to infer the model by observing its external behavior. This approach is useful when the source code of the system is not available, e.g., third party components. Regular inference techniques are able to infer a finite state machine model of a system by observing its external behavior.

We consider the models inferred by regular inference techniques of a certain kind of systems: communication protocol entities. Such entities interact by sending and receiving messages consisting of a message type and a number of parameters, each of which potentially can take on a large number of values. This may cause a model of a communication protocol entity inferred by regular inference, to be very large. Beside, since regular inference creates a model from the observed behavior of a communication protocol entity, the model may be very different from a designer's model of the system's source code.

I will present a novel approach to transform the inferred model of communication protocols to a new formalism in a sense that it is more compact and it has a similar partitioning of an entity's behavior into control states as in a designer's model of the protocol. We have applied our approach to an executable specification of the Mobile Arts Advanced Mobile Location Center (A-MLC) protocol and evaluated the results.

Tuesday, 23rd of June, 13:15, Nada library:
VCPT Demo and comparison to CoQ (Marco Dicola, and perhaps Karl P and/or Andreas)

Marco will give a brief demo on VCPT which will then be compared to an equivalent formulation in Coq.

Wednesday, 3rd of June, 13:15, Room 1635:
Temporal epistemic logic, model checking and abstraction (Mads Dam)

Followup on the talk Mads gave the 1st of April. We will pick up the trail about the "Muddy Children"-problem.

Wednesday, 13th of May, 13:00, Room 1635:
The IID algorithm. (Sindhu Muddassar)

Followup on previous talk.

Wednesday, 29th of April, 13:00, Room 1635:
The ID Algorithm (Sindhu Muddassar)

I will talk about Angluin's ID algorithm. This algorithm provides the foundation for our current work i.e. Incremental learning of Mealy machines. I will continue in the next talks for IID modification of this algorithm by R. Parekh et.al. and then later on our work about Incremental Learning of Mealy machines.
Angluin's ID algorithm is about learning a deterministic finite automaton (DFA) from a live complete set and a knowledgeable teacher. The teacher answers the queries posed by the learner from time to time. The learner stores the accepted set of results and refines the partitions of accepted strings in the table based on the feedback received from the teacher. When there are no more queries relevant to the live complete set, a DFA equivalent to the target DFA is constructed.

Wednesday, 8th of April, 13:00, Room 1635:
Learning based testing (Karl Meinke)

Karl will talk about what he, Fei and Muddassar are working on and lay a foundation for future talks by Fei and Muddassar.

Wednesday, 1st of April, 13:00, Room 1635:
Followup on the talk Mads gave the 18th (Mads Dam)

I will continue the talk from feb 18th and talk more about temporal epistemic logic, model checking and abstraction.

Wednesday, 25th of February, 13:00, Room 1635:
Security monitor inlining for multithreaded Java (Andreas Lundblad)

Program monitoring is about examining the execution of a program at runtime, and in our case terminate the program if it does something that is not considered to be secure. This can be realized by having some external intermediate security layer that either allows or disallows actions to proceed. In our work however we have chosen to embed (or inline) this layer into the program itself. When this is done in a multithreaded program some interesting questions arise, such as, what class of security policies can actually be securely enforced. In the presentation I'll try to explain a few of the issues and cover two or three theorems.

Wednesday, 18th of February, 13:00, Room 1635:
Linear Time Temporal Logic (LTL), Computational Tree Logic (CTL) and Epistemic Logic, Part 1 (Mads Dam)

A brief introduction to LTL, CTL and Epistemic Logic. We covered the basic syntax and semantics of the three different logics and their operators. We unraveled an LTS into a CTL tree, talked a little about the extension to CTL* and went through some example formulas in epistemic logic.