Wyniki wyszukiwania - BazTech

1

Quantification in frame semantics with binders and nominals of hybrid logic

Kallmeyer L., Osswald R., Pogodalla S.

Journal of Language Modelling

|

2017

|

Vol. 5, No. 2

357--383

EN

This paper aims to integrate logical operators into frame-based semantics. Frames are semantic graphs that allow lexical meaning to be captured in a fine-grained way but that do not come with a natural way to integrate logical operators such as quantifiers. The approach we propose stems from the observation that modal logic is a powerful tool for describing relational structures, including frames. We use its hybrid logic extension in order to incorporate quantification and thereby allow for inference and reasoning. We integrate our approach into a type theoretic compositional semantics, formulated within Abstract Categorial Grammars. We also show how the key ingredients of hybrid logic, nominals and binders, can be used to model semantic coercion, such as the one induced by the begin predicate. In order to illustrate the effectiveness of the proposed syntax-semantics interface, all the examples can be run and tested with the Abstract Categorial Grammar development toolkit.

2

Monitoring with Parametrized Extended Life Sequence Charts

Chai M., Schlingloff B. -H.

Fundamenta Informaticae

|

2017

|

Vol. 153, nr 3

173--198

EN

Runtime verification is a lightweight formal method that checks whether an execution of a system satisfies a given property. A challenge in building a runtime verification system is to define a suitable monitoring specification language, i.e., a language that is expressive, of reasonable complexity, and easy to understand. In this paper, we extend live sequence charts (LSCs, [1]) for the specification of properties in systems monitoring. We define Parametrized extended LSCs (PeLSCs) by introducing the notions of necessary prechart, concatenation, and conditionand assignment-structure. With these PeLSCs, necessary and sufficient conditions of certain observations, and parametric properties can be specified in an intuitive way. We prove some results about the expressiveness of extended LSCs. In particular, we show that LSCs with necessary precharts are strictly more expressive than standard LSCs, and that iteration-free extended LSCs have the same expressive power as linear temporal logic (LTL). To generate monitors, we develop translations of PeLSCs into hybrid logic. We show that the complexity of the word problem of PeLSCs is linear with respect to the length of input traces, thus our formalism is well-suited for online monitoring of communicating systems.

3

Automata-Theoretic Decision Procedures for Information Logics

Demri S., Sattler U.

Fundamenta Informaticae

|

2002

|

Vol. 53, nr 1

1-22

EN

Automata-theoretic decision procedures for solving model-checking and satisfiability problems for temporal, dynamic, and description logics have flourished during the past decades. In the paper we define an EXPTIME decision procedure based on the emptiness problem of Büchi automata on infinite trees for the very expressive information logic SIM designed for reasoning about information systems. This logic involves modal parameters satisfying certain properties to capture the relevant nominals at the formula level, Boolean expressions and nominals at the modal level, an implicit intersection operation for relations, and a universal modality. The original combination of known techniques allows us to solve the open question related to the EXPTIME -completeness of SIM. Furthermore, we discuss how variants of SIM can be treated similarly although the decidability status of some of them is still unknown.