PROGRAM FOR WEDNESDAY, JUNE 25TH

ABSTRACT. Model Checking is an automatic verification technique for large state transition systems. It was originally developed for reasoning about finite-state 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.

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 branching-time 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 variability-specific modal logic and the associated special-purpose model checker VMC. As a result, it offers the possibility to efficiently verify formulas over possibly infinite-state systems by using the on-the-fly bounded model-checking algorithms implemented in the model checker. We illustrate our approach by means of a simple yet intuitive example: a bike-sharing system.

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 multi-valued model checking can distinguish conclusive and inconclusive results, while increasing precision over tradi- tional two-valued over- and under-abstractions. This paper describes the theory and implementation of multi-valued model checking for Promela specifications. We believe our tool Bonsai is the first four-valued model checker capable of multi-valued 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.

ABSTRACT. We present a novel method for reasoning about time in state-based proof-oriented formalisms. The method builds on a non-classical 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 Event-B formalism. We illustrate the method with a machine-checked proof of Fischer's algorithm that, to our knowledge, is simpler than other proofs available in the literature.

ABSTRACT. Launchbury defines a natural semantics for lazy evaluation and proposes an alternative call-by-name 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 beta-reduction 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.

ABSTRACT. The Function Blocks Architecture of the IEC 61499 standard is an executable component model for distributed embedded control systems combining block-diagrams 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 model-checker 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 model-checking is illustrated for a simple test case.

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.

ABSTRACT. The term Linked Data is used to describe ubiquitous and emerging semi-structured data formats on the Web that allows diverse data sources to link to each other, forming a Web of Data. We present a language-based 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.

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.

ABSTRACT. The intention of the note is towards a framework for developing, studying and comparing observational semantics in the setting of a real-time 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 linear-time -- branching-time 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.

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 thp-bisimulation.

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 non-temporal reasoning, and prove that we obtain a complete axiomatization relative to the non-temporal base logic dL. Using this calculus, we analyze metric temporal safety properties in a local lane control system.

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 weighted-bisimilarity of LWSs. In addition, we prove that the logic is decidable, i.e., the satisfiability problem for RWL can be algorithmically solved.

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 real-valued functions, a sufficiently simple index set of the class reflects its simplicity. We construct computable numberings for effectively open sets and computable real-valued 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 Rice-Shapiro theorem for effectively open sets of reals and an analogue of Rice theorem for computable real-valued functions. We illustrate how index sets can be used to estimate complexity of continuous constraints in settings of Kleene-Mostowski arithmetical hierarchy.

ABSTRACT.  

Disjoint AND-decomposition 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 AND-decompositions 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 well-known NP-complete Hypergraph 2-Coloring Problem.

ABSTRACT. The paper presents a multi-agent approach for ontology population based on natural language semantic analysis. In this multi-agent 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 semantic-syntactic model of the language.