Wyniki wyszukiwania - BazTech

1

Towards Syntactic Epistemic Logic

Artemov Sergei

Fundamenta Informaticae

|

2022

|

Vol. 186, nr 1-4

49--62

EN

Traditionally, Epistemic Logic represents epistemic scenarios using a single model. This, however, covers only complete descriptions that specify truth values of all assertions. Indeed, many -- and perhaps most -- epistemic descriptions are not complete. Syntactic Epistemic Logic, SEL, suggests viewing an epistemic situation as a set of syntactic conditions rather than as a model. This allows us to naturally capture incomplete descriptions; we discuss a case study in which our proposal is successful. In Epistemic Game Theory, this closes the conceptual and technical gap, identified by R. Aumann, between the syntactic character of game-descriptions and semantic representations of games.

2

Solving Infinite Games in the Baire Space

Brütsch Benedikt, Thomas Wolfgang

Fundamenta Informaticae

|

2022

|

Vol. 186, nr 1-4

63--88

EN

Infinite games (in the form of Gale-Stewart games) are studied where a play is a se- quence of natural numbers chosen by two players in alternation, the winning condition being a subset of the Baire space ωω . We consider such games defined by a natural kind of parity au- tomata over the alphabet N, called N-MSO-automata, where transitions are specified by monadic second-order formulas over the successor structure of the natural numbers. We show that the classical Büchi-Landweber Theorem (for finite-state games in the Cantor space 2ω) holds again for the present games: A game defined by a deterministic parity N-MSO-automaton is deter- mined, the winner can be computed, and an N-MSO-transducer realizing a winning strategy for the winner can be constructed.

3

A Note on Calculi for Non-deterministic Many-valued Logics

Kaminski Michael

Fundamenta Informaticae

|

2022

|

Vol. 186, nr 1-4

143--153

EN

We present two deductively equivalent calculi for non-deterministic many-valued log ics. One is defined by axioms and the other – by rules of inference. The two calculi are obtained from the truth tables of the logic under consideration in a straightforward manner. We prove soundness and strong completeness theorems for both calculi and also prove the cut elimination theorem for the calculi defined by rules of inference.

4

On the Expressive Power of Non-deterministic and Unambiguous Petri Nets over Infinite Words

Finkel Olivier, Skrzypczak Michał

Fundamenta Informaticae

|

2021

|

Vol. 183, nr 3-4

243--291

EN

To identify the causes of performance problems or to predict process behavior, it is essential to have correct and complete event data. This is particularly important for distributed systems with shared resources, e.g., one case can block another case competing for the same machine, leading to inter-case dependencies in performance. However, due to a variety of reasons, real-life systems often record only a subset of all events taking place. To understand and analyze the behavior and performance of processes with shared resources, we aim to reconstruct bounds for timestamps of events in a case that must have happened but were not recorded by inference over events in other cases in the system. We formulate and solve the problem by systematically introducing multi-entity concepts in event logs and process models. We introduce a partial-order based model of a multi-entity event log and a corresponding compositional model for multi-entity processes. We define PQR-systems as a special class of multi-entity processes with shared resources and queues. We then study the problem of inferring from an incomplete event log unobserved events and their timestamps that are globally consistent with a PQR-system. We solve the problem by reconstructing unobserved traces of resources and queues according to the PQR-model and derive bounds for their timestamps using a linear program. While the problem is illustrated for material handling systems like baggage handling systems in airports, the approach can be applied to other settings where recording is incomplete. The ideas have been implemented in ProM and were evaluated using both synthetic and real-life event logs.