PROGRAM FOR WEDNESDAY, JUNE 25TH
View: session overviewtalk overview
09:00  Model Checking and the Verification of Computer Systems SPEAKER: Ed Clarke ABSTRACT. Model Checking is an automatic verification technique for large state transition systems. It was originally developed for reasoning about finitestate concurrent systems. The technique has been used successfully to debug complex computer hardware and communication protocols. Now, it is beginning to be used for software verification as well. The major disadvantage of the technique is a phenomenon called the State Explosion Problem. This problem is impossible to avoid in worst case. However, by using sophisticated data structures and clever search algorithms, it is now possible to verify state transition systems with astronomical numbers of states.

10:00  Model Checking ValuePassing Modal Specifications SPEAKER: Maurice H. Ter Beek ABSTRACT. Formal modelling and verification of variability concepts in product families has been the subject of extensive study in the literature on Software Product Lines. In recent years, we have laid the basis for the use of modal specifications and branchingtime temporal logics for the specification and analysis of behavioural variability in product family definitions. A critical point in this formalization is the lack of a possibility to model an adequate representation of the data that may need to be described when considering real systems. To this aim, we now extend the modelling and verification environment that we have developed for specifications interpreted over Modal Transition Systems, by adding the possibility to include data in the specifications. In concert with this, we also extend the variabilityspecific modal logic and the associated specialpurpose model checker VMC. As a result, it offers the possibility to efficiently verify formulas over possibly infinitestate systems by using the onthefly bounded modelchecking algorithms implemented in the model checker. We illustrate our approach by means of a simple yet intuitive example: a bikesharing system. 
10:55  Bonsai: Cutting Models Down to Size SPEAKER: unknown ABSTRACT. In model checking, abstractions can cause spurious results, which need to be verified in the concrete system to gain conclusive res ults. Verification based on multivalued model checking can distinguish conclusive and inconclusive results, while increasing precision over tradi tional twovalued over and underabstractions. This paper describes the theory and implementation of multivalued model checking for Promela specifications. We believe our tool Bonsai is the first fourvalued model checker capable of multivalued verification of parallel models, i.e. con sisting of multiple concurrent processes. A novel aspect is the ability to only partially abstract a model, keeping parts of it concrete. 
11:20  A proofbased method for modelling timed systems SPEAKER: Alexei Iliasov ABSTRACT. We present a novel method for reasoning about time in statebased prooforiented formalisms. The method builds on a nonclassical model of time, the Leibnizian model, in which time is a relative property determined by the observations of an evolving subject, rather than one of the fundamental dimensions. It proves to be remarkably effective in the context of the EventB formalism. We illustrate the method with a machinechecked proof of Fischer's algorithm that, to our knowledge, is simpler than other proofs available in the literature. 
11:45  The role of indirections in lazy natural semantics SPEAKER: unknown ABSTRACT. Launchbury defines a natural semantics for lazy evaluation and proposes an alternative callbyname version which introduces indirections and does not update closures. The equivalence of both semantics is not straightforward. In the present paper we focus on the introduction of indirections during betareduction and study how the heaps, i.e., the sets of bindings, obtained with this kind of evaluation do relate with the heaps produced by substitution. As a heap represents the context of evaluation for a term, we first define an equivalence that identifies terms with the same meaning under a given context. This notion of "context" equivalence is extended to heaps. Finally, we define a relation between heap/term pairs to establish the equivalence between Launchbury's alternative natural semantics and its corresponding version without indirections. 
12:10  Neutralizing Semantic Ambiguities of Function Block Architecture by Modeling with ASM SPEAKER: unknown ABSTRACT. The Function Blocks Architecture of the IEC 61499 standard is an executable component model for distributed embedded control systems combining blockdiagrams and state machines. The standard aims at the portability of control applications that is however hampered by ambiguities in its execution semantics descriptions. In recent years several execution models have been implemented in different software tools that generate mutually incompatible code. This paper proposes a general approach to neutralizing these semantic ambiguities by formal description of the IEC 61499 in abstract state machines (ASM). The model embodies all known execution semantics of function blocks. The ASM model is further translated to the input format of the SMV modelchecker which is used to verify formally properties of applications. In this way the proposed verification framework enables the portability checking of component based control applications across different implementation platforms compliant with the IEC 61499 standard. The paper first discusses different existing execution semantics of function blocks and the portability issues across different IEC 61499 tools. Then a modular formal model of function blocks’ operational semantics in ASM is introduced and exemplified in the paper by the cyclic execution semantics case for a composite function block. Subsequently, the SMV model is generated and modelchecking is illustrated for a simple test case. 
12:35  Probabilistic formal concepts for contexts with negation SPEAKER: unknown ABSTRACT. The probabilistic generalization of formal concept is presented: construction is resistant to noise in the data and give one an opportunity to consider both the attribute and it's absence (context with negation). This generalization is obtained from the notion of formal concepts through its denition as xed points of implications. Then implications, possibly with negations, are replaced by probabilistic laws. We prove that the xed points based on the probabilistic implications are consistent and thus determine the probabilistic formal concepts. Correspondence between probabilistic formal concepts and classic formal concepts is also presented. Previously the following was conrmed experimentally: if the formal concepts are found on some data and are swayed with some random noise, then the noisy data context allows the complete reconstruction of initial formal context's concepts. In the end, the demonstration for the probabilistic formal concepts formation is given. 
14:00  Languages and types for linked data SPEAKER: Vladimiro Sassone ABSTRACT. The term Linked Data is used to describe ubiquitous and emerging semistructured data formats on the Web that allows diverse data sources to link to each other, forming a Web of Data. We present a languagebased model which captures concurrent queries and updates over Linked Data. The calculus exhibits operations essential for declaring rich atomic actions and recovers emergent structure in the loosely structured Web of Data. A light type system ensures that URIs with a distinguished role are used consistently. The main theorem verifies that the light type system and operational semantics work at the same level of granularity, so are compatible. 
15:00  Process Opacity SPEAKER: Damas Gruska ABSTRACT. A new security concept called {\em process opacity} is formalized and studied. For processes which are process opaque with respect to a given predicate over processes, an intruder cannot learn validity of this predicate for any subsequent state of computation. We discuss different extensions of this concept as well as its properties. We put some restrictions on predicates in such a way that we obtain decidable security properties. 
15:15  Comparing Semantics under Strong Timing of Petri Nets SPEAKER: unknown ABSTRACT. The intention of the note is towards a framework for developing, studying and comparing observational semantics in the setting of a realtime true concurrent model. In particular, we introduce trace and bisimulation equivalences based on interleaving, step and causal net semantics in Petri nets with strong timing. We treat the relationships between the equivalences showing the discriminating power of the approaches of the lineartime  branchingtime and interleaving  partial order spectra. The results obtained allow one to study in complete detail the timing behaviour in addition to the degrees of relative concurrency and nondeterminism of processes. 
15:30  Timed History Preserving Bisimulation and Open Maps SPEAKER: Natalya Gribovskaya ABSTRACT. In recent decades, the open maps approach has been successfully applied to structure and unify a wide range of behavior equivalences for concurrency. In this paper, we will prove that timed history preserving (thp) bisimulation can be captured by the natural instance of an open maps bisimilarity when timed causal trees are chosen as the model category. In particular, we will define a category of timed causal trees and an accompanying subcategory of causal timed words, for which the notion of open maps will be developed. Then we will use the open maps framework to obtain an abstract bisimilarity. Finally, we will establish the coincidence of the obtained abstract bisimilarity and thpbisimulation. 
15:45  Verification of Temporal Properties of Hybrid Systems Using dMTL SPEAKER: Ping Hou ABSTRACT. We introduce a logic for verifying metric temporal properties of hybrid systems that combines differential dynamic logic (dL) for reasoning about the possible behavior of hybrid systems with metric temporal logic (MTL) for reasoning about the metric temporal behavior during their operation. For our logic, we generalize the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dL for hybrid systems. On this basis, we provide a modular verification calculus that reduces correctness of metric temporal behavior of hybrid systems to generic temporal reasoning and then nontemporal reasoning, and prove that we obtain a complete axiomatization relative to the nontemporal base logic dL. Using this calculus, we analyze metric temporal safety properties in a local lane control system. 
16:30  Decidability and Expressiveness of Recursive Weighted Logic SPEAKER: Bingtian Xue ABSTRACT. Labeled weighted transition systems (LWSs) are transition systems labeled with actions and real numbers. These numbers represent the costs of the corresponding actions in terms of resources. Recursive Weighted Logic (RWL) is a multimodal logic that expresses qualitative and quantitative properties of LWSs. It is endowed with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We demonstrate that RWL is sufficiently expressive to characterize weightedbisimilarity of LWSs. In addition, we prove that the logic is decidable, i.e., the satisfiability problem for RWL can be algorithmically solved. 
16:55  Index sets as a measure of continuous constraint complexity SPEAKER: unknown ABSTRACT. We introduce and study the theory of index sets in the context of computable analysis. If we consider a class of effectively open sets or a class of computable realvalued functions, a sufficiently simple index set of the class reflects its simplicity. We construct computable numberings for effectively open sets and computable realvalued functions and show that these numberings are principal. We calculate index sets for important problems such as root realisability, set equivalence and inclusion, function equivalence which naturally arise in continuous constraint solvability. Using developed techniques we present clear proofs of generalised RiceShapiro theorem for effectively open sets of reals and an analogue of Rice theorem for computable realvalued functions. We illustrate how index sets can be used to estimate complexity of continuous constraints in settings of KleeneMostowski arithmetical hierarchy. 
17:20  On Tractability of Disjoint ANDDecomposition of Boolean Formulas SPEAKER: Pavel Emelyanov ABSTRACT. Disjoint ANDdecomposition of a boolean formula means its representation as a conjunction of two (or several) formulas having disjoint sets of variables. We show tractability of computing ANDdecompositions of boolean formulas given in ANF, Full DNF, and positive DNF. As an important tool for proving tractability, we provide a polytime algorithm for factoring linear multivariate polynomials over the finite field of order 2 and note that it is related to a variant of the wellknown NPcomplete Hypergraph 2Coloring Problem. 
17:35  A Multiagent Text Analysis Based on Ontology of Subject Domain SPEAKER: Natalia Garanina ABSTRACT. The paper presents a multiagent approach for ontology population based on natural language semantic analysis. In this multiagent model agents of two main kinds interact: the information agents correspond to meaningful units of the information being retrieved, and the rule agents implement population rules of a given ontology and a semanticsyntactic model of the language. 