Fundamenta Informaticae - Volume 36, issue 1

Authors: Bhat, Girish | Peled, Doron

Article Type: Research Article

Abstract: Modeling execution as partial orders increases the flexibility in reasoning about concurrent programs by allowing the use of alternative, equivalent execution sequences. This is a desirable feature in specifying concurrent systems which allows formalizing frequently used arguments such as ‘in an equivalent execution sequence’, or ‘in a consistent global state, not necessarily on the execution sequence’ to be formalized. However, due to the addition of structure to the model, verification of partial order properties is non-trivial and sparse. We present here a new approach which allows expressing and verifying partial order properties. It is based on modeling an execution as …a linear sequence of global states, where each state is equipped with its past partial-order history. The temporal logic BPLTL (for Branching Past Linear Temporal Logic) is introduced. We provide a sound and relatively complete proof system for the logic BPLTL over transitions programs. Our proof system augments an existing proof system for LTL. Show more

DOI: 10.3233/FI-1998-3611

Citation: Fundamenta Informaticae, vol. 36, no. 1, pp. 1-21, 1998

Authors: Doherty, Patrick | Łukaszewicz, Witold | Szałas, Andrzej

Article Type: Research Article

Abstract: We first define general domain circumscription (GDC) and provide it with a semantics. GDC subsumes existing domain circumscription proposals in that it allows varying of arbitrary predicates, functions, or constants, to maximize the minimization of the domain of a theory. We then show that for the class of semi-universal theories without function symbols, that the domain circumscription of such theories can be constructively reduced to logically equivalent first-order theories by using an extension of the DLS algorithm, previously proposed by the authors for reducing second-order formulas. We also show that for a certain class of domain circumscribed theories, that any …arbitrary second-order circumscription policy applied to these theories is guaranteed to be reducible to a logically equivalent first-order theory. In the case of semi-universal theories with functions and arbitrary theories which are not separated, we provide additional results, which although not guaranteed to provide reductions in all cases, do provide reductions in some cases. These results are based on the use of fixpoint reductions. Show more

DOI: 10.3233/FI-1998-3612

Citation: Fundamenta Informaticae, vol. 36, no. 1, pp. 23-55, 1998

Authors: Rahonis, George | Salomaa, Kai

Article Type: Research Article

Abstract: We consider classes of forests defined by synchronized and pushdown tree automata having a fixed size of, respectively, synchronization or pushdown alphabet. We show that such families have nice properties, for instance, they form either a sheaf or a strict alphabetic cone of forests. Furthermore, for the (deterministic and nondeterministic) synchronized tree automata and the real-time pushdown tree automata we obtain a strict infinite forest hierarchy with respect to the alphabet size.

Keywords: tree automata, synchronization, pushdown stores

DOI: 10.3233/FI-1998-3613

Citation: Fundamenta Informaticae, vol. 36, no. 1, pp. 57-69, 1998

Authors: Winkowski, Józef

Article Type: Research Article

Abstract: Generalized Place/Transition Petri nets, called contextual nets, and processes of such nets are considered. Processes of contextual nets are represented as partial orders with some extra structure. Operations of composing processes are defined such that each process of a contextual net can be obtained by combining processes corresponding to places and transitions of this net. Matrix-like characteristics of processes, called tables, and natural operations on such characteristics are defined such that the correspondence between processes and their characteristics is a homomorphism.

Keywords: Contextual net, process, sequential composition, parallel composition, interchange, table, table multiplication, juxtaposition of tables, interchange of tables, homomorphism

DOI: 10.3233/FI-1998-3614

Citation: Fundamenta Informaticae, vol. 36, no. 1, pp. 71-101, 1998