ICS PAS Reports

Abstract: : A general semantics of strategic abilities of agents in asynchronous systems with and without perfect information is proposed, and some general complexity results for verification of strategic abilities in asynchronous systems are presented. A methodology for partial order reduction (POR) in verification of agents with imperfect information is developed, based on the notion of traces introduced by Mazurkiewicz. Two semantics of ATL*_x are considered and it is shown that for memoryless imperfect information (|=ir) contrary to memoryless perfect information (|=Ir), one can apply techniques known for LTL_x.

Keywords: Alternating-Time Temporal Logic, asynchronous systems, partial order reduction, traces

Abstract: In the paper a model of action is described that is universal in the sense that it may serve to represent actions of any kind: discrete, continuous, or partially discrete and partially continuous. The model is founded on the assumption that an action is executed in a universe of objects. It describes how the possible executions change the situation of involved objects. It exploits the fact that executions are represented such that fragments of executions are represented such that their closed segments admit only trivial automorphisms. The model has an algebraic strucure and it is a directed complete partial order.

Keywords: Action, object, object instance, occurrence of object instance, execution, execution segment, execution fragment, execution structure, lposet, pomset, sequential composition, parallel composition, independent component, prefix order

Abstract: : The paper is the revision, extended and full version of the short (6 pages) preliminary presentation of the grounding of the notion of Continuum given in Section 6 of the paper Types and operations ICS PAS Report No. 1030 (also at http://arxiv.org/abs/1501.03043). Here, primitive types (corresponding to the intuitive concept of Continuum) are introduced along with primitive operations, constructors, and relations. The paper is also at arXiv http://arxiv.org/abs/1510.02787

Keywords: Continuum, types, semantics, foundations of Mathematics

Abstract: : The paper describes structures which can be used to represent activities of broad class. The concept of event structure is generalized to represent activities which may be discrete, continuous, or of mixed nature. Con_guration structures of the more general event structures are used to deńe axiomatically con_guration domains. Elements of such domains are abstract representants of runs of represented activities. The partial order of elements reects how each run extends to longer runs. It is shown that con_guration domains deńe event structures which can be interpreted as interactions of sets of objects.

Keywords: Activity, run, event, causal dependency relation, conict relation, event structure, con_guration, con_guration structure, partially ordered set, directed complete partially ordered set, con_guration domain, transition, region.

Abstract: : We investigate the correspondence between model checking of af-AMCi and ATLir , on the example of reachability. We identify some of the reasons for the fact that these logics are of uncomparable expressivity. These observations form the basis for a novel method for underapproximating ATLir by means of fixed-point calculations. We introduce a special version of the next-step operator, called Persistent Imperfect Next-Step Operator h_iF and show how it can be used to define a new version of reachability that carries to ATLir.

Keywords: ATL, model checking, approximation

Abstract: : The paper describes an application of a graph database to the abstract planning in the Planics composition system for web services. Abstract planning is the first stage of the service composition process, and consists in matching types of the services and objects processed by them, with some additional constraints. The result is an abstract plan matching the user query. The presented solution prunes the ontologies for the abstract planners, greatly improving efficiency and providing better scalability. This is of particular importance in the domain of web service composition, because usually systems are expected to produce answers immediatly.

Keywords: automatic composition of web services, graph databases, abstract planning

Abstract: : A revision of the basic concepts of type, function (called here operation), and relation is proposed. A simple generic method is presented for constructing operations and types as concrete nite structures parameterized by natural numbers. The method gives rise to build inductively so called Universe intended to contain all what can be e ectively constructed at least in the sense assumed in the paper. It is argued that the Universe is not yet another formal theory but may be considered as a grounding for some formal theories.

Keywords: types, semantics, foundations

Abstract: : In the paper a model of action is described that is universal in the sense that it may serve to represent actions of any kind: discrete, continuous, or partially discrete and partially continuous. The model is founded on the assumption that an action is executed in a universe of objects. It describes how the possible executions change the situation of involved objects. It exploits the fact that executions are represented such that their bounded segments admit only trivial automorphisms. Consequently, the model has an algebraic strucure and is a directed complete partialorder.

Keywords: Action, object, object instance, occurrence of object instance, concrete execution, execution structure, history preserving equivalence of concrete execution structures, abstract execution, algebra of abstract executions, directed complete partialorder, reduced execution structure.

Abstract: : This paper defines a temporal logic for reaction systems (RSTL). The logic is interpreted over the models for the context restricted reaction systems that generalize standard reaction systems by controlling context sequences. Moreover, a translation from the context restricted reaction systems into boolean functions is defined in order to be used for a symbolic model checking for RSTL over these systems. Finally, model checking for RSTL is proved to be PSPACE-complete.

Keywords: reaction systems, model checking, temporal logic

Abstract: : The paper deals with the abstract planning problem - the first stage of Web Service Composition (WSC) in the Planics framework. We present a solution based on a compact repre-sentation of abstract plans by multisets of service types and a reduction of the planning problem to a task for an SMT-solver. The paper presents theoretical aspects of the abstract planning as well as some details of our symbolic encoding and implementation, followed by preliminary experimental results.

Keywords: Web Service Composition, SMT, Abstract Planning

Abstract: : The paper presents a new approach based on nature inspired algorithms to an automated abstract planning problem, which is a part of the web service composition problem. An abstract plan is defined as an equivalence class of sequences of service types that satisfy a user query. Intuitively, two sequences are equivalent if they are composed of the same service types, but not necessarily occurring in the same order. The objective of our genetic algorithm (GA) is to return representatives of abstract plans without generating all the equivalent sequences. The paper presents experimental results, which show that GA finds solutions for very large sets of service types in a reasonable time.

Keywords: genetic algorithms, web service composition, abstract planning

Abstract: : The present report discusses the principles of lexical-semantic annotation of treebank Składnica by means of Słowosiec (PlWordNet) lexical units. Moreover, it presents a method of mapping NKJP named entities annotation to Składnica (including evaluation). All three resources mentioned above are shortly described. Finally, a method of updating the annotation to changes appearing both in Słowosiec and Składnica.

Keywords: computational linguistics, text corpora, treebanks, corpora annotation, lexical semantics, wordnet

Title: Semantic Annotation of Treebank Składnica Fundamentals, named entities, actualisation (paper written in polish)

Abstract: : The paper presents a theoretical basis for decribing and analysing random behaviours of concurrent systems of a broad class. Keywords: concurrent system, state, process, composition, labelled poset, pomset, directed complete partial order, Scott topology, Borel σ-algebra of sets probability measure

Abstract: : The paper contributes with a concept of process viewed as a model of a run of a system (discrete, continuous, or of a mixed type), with operations allowing to define complex processes in terms of their components, and with the idea of using the formal tools thus obtained to define the behavionrs of concurrent systems.

A process may have an initial state (a source), a final state (a target), or both. Processes of which one is a continuation of the other can be composed sequentially. Independent processes, ie. processes which do not disturb each other, can be composed in parallel. Processes may be prefixes, i.e. independent components of initial segments of other processes. Processes and operations on processes are represented by partially ordered multisets of a certain type and operations on such multisets.

Processes in a universe of objects and the sequential composition of processes form a partial category, called a partial category of processes. Processes in a universe of objects and the operations of composing processes seąnentially and in parallel form a partial algebra, called an algebra of processes. Partial categories and algebras of processes belong to axiomatically defined classes of partial algebras, called behaviour-oriented partial categories and behaviour-oriented algebras. Some of behaviour-oriented partial categories and behaviour-oriented algebras can be represented as partial categories of proces es and algebras of processes.

Partial categories and algebras of processes can be used to define behaviours of concurrent systems. Namely, the behaviour of a system can be defined as the set of possible processes of this system with a structure on this set. The stucture reflexes the prefix order and makes the set of possible processes a directed complete poset.

Partial categories and algebras of processes can also be used to define behaviours with states and processes provided with specific structures, to define operations on behaviours similar to those in the existing calculi of behaviours, and to define random behaviours.

Keywords: Process, state, sequential composition, parallel composition, category, partial category, partial monoid, independence, region, structure, behaviour, random behaviour.

Abstract: : The present report describes the most famous corpora of natural language texts. First, the rules of corpora construction are analysed, namely, determining its structure and selecting texts to be included in the corpus. Next, the most popular corpora are presented. The majority of them are English corpora, but corpora of other European languages: French, German, Czech and Russian are considered as well. The special attention is paid to two Polish corpora: the IPI PAN Corpus and the National Corpus of Polish. The separate section is devoted to treebanks, i.e., corpora that are syntactically annotated.

Keywords: computational linguistics, text corpora, treebanks, corpora annotation

Title: Most popular text corpora. The survey (paper written in polish)

Abstract: : The present report describes initial experiments on syntactic-semantic classification of Polish verbs. First, the existing works on this subject were discussed, mainly concerning English. Second, Grade Correspondence-Cluster Analysis used in experiments was described. Next, syntactic-semantic valence dictionary of Polish verbs being a source of data for experiments was presented. Finally, actual experiments were discussed and evaluated.

Keywords: computational linguistics, lexical semantics, electronic valence dictionaries, verb classification, selectional preferences, wordnet

Title: Experiments on classifying verbs in a semantic dictionary of Polish (paper written in polish)