Abstracts of Fundamenta Informaticae Volume 36 


Adding Partial Orders to Linear Temporal Logic
Girish Bhat and  Doron Peled
pages 1-21

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.

General Domain Circumscription and its Effective Reductions
Patrick Doherty, Witold Łukaszewicz and Andrzej Szałas
pages 23-55

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.

On the Size of Stack and Synchronization Alphabets of Tree Automata
George Rahonis and  Kai Salomaa
pages 57-69

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 lphabet size.

Processes of Contextual Nets and their Characteristics
Józef Winkowski
pages 71-101

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.


Remarks on the Relationship Between Cooperating Distributed Grammar Systems and Lindenmayer Systems
Mohamed Amin
pages 103-107

In [DassowPaunVicolov]it is shown that the family of languages generated by cooperating distributed (CD) grammar systems with context-free components in the derivation modes $=k, ge k$, for $kge 2$, and the family of E0L languages are incomparable. Because one of the languages used in the proof of the incomparability does not work, we fill here the gap, using another language. We also give an effective procedure for constructing an  ET0L system from a given context-free cooperating/distributed (CD) grammar system working in the maximum mode of cooperation.
On the Semantics of a Semantic Network
Anastasia Analyti,  Nicolas Spyratos,  Panos Constantopoulos
pages 109-144

We elaborate on the semantics of an enhanced object-oriented semantic network, where  multiple instantiation, multiple
specialization, and meta-classes are supported for both kinds of objects: entities and properties. By semantics of a semantic network, we mean the information (both explicit and derived) that the semantic network carries. Several data models use semantic networks to organize information. However, many of these models do not have a formalism defining what the semantics of the semantic network is.
In our data model, in addition to the Isa relation, we consider a stronger form of specialization for properties, that we call  restriction isa, or Risa for short. The Risa relation expresses property value refinement.  A distinctive feature of our data model is that it supports the interaction between Isa and Risa relations. The combination of  Isa and Risa provides a powerful conceptual modeling mechanism.
The user declares objects and relations between objects through a program. Reasoning is done through a number of (built-in) em inference rules that allow for derivations both at instance and schema level. Through the inference rules, new objects and new relations between objects are derived. In our data model, inherited properties are considered to be derived objects. In addition to the inference rules, a number of (built-in) em system constraints exist for checking the validity of a program.

Characterization of the Expressive Power of Silent Transitions in Timed Automata
Beatrice Berard, Antoine Petit,  Volker Diekert and Paul Gastin

Timed automata are among the most widely studied models for real-time systems.  Silent transitions, i.e., epstrs, have already been proposed in the original paper on timed automata by Alur and Dill [AD90].  We show that the class tle of timed languages recognized by automata with epstrs, is more robust and more expressive than the corresponding class tl without epstrs.
We then focus on epstrs without reset, i.e. epstrs which do not reset clocks.  We propose an algorithm to construct, given a timed automaton, an equivalent one without such transitions.  This algorithm is in two steps, it first suppresses the cycles of epstrs without reset and then the remaining ones.
Then, we prove that a timed automaton such that no epstr which resets clocks lies on any directed cycle, can be effectively
transformed into a timed automaton without epstrs.  Interestingly, this main result holds under the assumption of non-Zenoness and it is false otherwise.
To complete the picture, we exhibit a simple timed automaton with an epstr, which resets some clock, on a cycle and which is not equivalent to any $varepsilon$-free timed automaton.  To show this, we develop a promising new technique based on the notion of precise action.
This paper presents a synthesis of the two conference communications [BGP96] and [DGP97].

Remarks on Operations Suggested by Mutations in Genomes
Jurgen Dassow and Gheorghe Paun
 pages 183-200

In the last years the operation of splicing which models a special type of recombination of genomes has been intensively studied, e.g. the effect of application of splicings to language families of classical formal language theory has been investigated. In this paper we present analogous results with respect to the operations inversion, translocation and duplication which are also descriptions of mutations of genomes.

A Uniform Axiomatic View of Lists, Multisets, and Sets, and the Relevant Unification Algorithms
Agostino Dovier, Alberto Policriti, Gianfranco Rossi
pages 201-234

The first-order theories of lists, multisets, compact lists (i.e., lists where the number of contiguous occurrences of each element is immaterial), and sets are introduced via axioms. Such axiomatizations are shown to be very well-suited for the
integration with free functor symbols governed by the classical Clark's axioms in the context of (Constraint) Logic Programming. Adaptations of the extensionality principle to the various theories taken into account is then exploited in the design of unification algorithms for the considered data structures. All the theories presented can be combined providing frameworks to deal with several of the proposed data structures simultaneously. The unification algorithms proposed can be combined (merged) as well, to produce engines for such combination theories.

Truth of Duration Calculus Formulae in Timed Frames
C.A. Middelburg
pages 235-263

Duration calculus is a logical formalism designed for expressing and refining real-time requirements for systems.
Timed frames are essentially transition systems meant for modeling the time-dependent behaviour of programs. We investigate the interpretation of duration calculus formulae in timed  frames. We elaborate this topic from different angles and show that they agree with each other. The resulting interpretation is expected to make it generally easier to establish semantic links between duration calculus and formalisms aimed at programming. Such semantic links are prerequisites for a solid underpinning of approaches to system development that cover requirement capture through coding using both duration calculus and some formalism(s) aimed at programming.

Optimizations of Rough Set Model
Jarosław Stepaniuk
pages 265-283

Rough set methodology is based on concept (set) approximations constructed from available background knowledge represented in information systems cite [Pa91]. In many applications only partial knowledge about approximated concepts is given. Hence quite often first a parametrized family of concept approximations is built and next by tuning of the parameters the best, in a sense, approximation is chosen (see e.g. variable precision rough set model [Zi93]) in approximation spaces. In this paper we follow this approach in generalized approximation spaces. We discuss rough set model based on approximation spaces with uncertainty functions and rough inclusions. Both elements of approximation space are  parametrized and for the proper application of such model to a particular data set it is necessary to make optimization of the parameters. We discuss basic properties of the mentioned model and also strategies of parameters optimization. We also present different notions of rough relations. Optimization of different parameters can be based on degree of inclusion of relations defined by condition and decision attributes. Some illustration of presented methods on real medical data set is
also included.

On Entropy and Optimal Coding Cost for Stochastic Language
Larissa Zhiltsova
pages 285-305

We investigate questions, relating to optimal binary coding of a language, for which a probability distribution is given on its words (for a stochastic language). As optimal we understand the coding, which gives minimum of mathematical expectation of a length of the coded word, or minimum of the coding cost.
For any stochastic language with a finite value of the entropy we establish lower and upper bounds of the optimal coding cost, dependent only on the entropy, and we prove their unimprovability.
For any stochastic context-free language with unique derivation it is found necessary and sufficient condition of existence of finite values of the optimal coding cost and the entropy. Also an effective method of calculation of the entropy is found for the case when the considered condition holds.



On the Average-Case Complexity of the Graph Reliability Problem on Gaussian Distributions
Dmitri Burago and Michel de Rougemont
pages 307-315
We introduce classes of narrow graphs (including grid strips of fixed width), for which the graph reliability problem admits a polynomial time algorithm. Using this algorithm, we show that graph reliability is computable in polynomial time for the average complexity with respect to a Gaussian distribution. The latter is defined as follows: the vertices are numbered by integers 1,2, ...,n, and the probability that an edge between i and j is present is e^(-|i-j|^2).

Randomized PRAM Simulation

Zbigniew J. Czech and Wojciech Mikanik
pages 317-336

The parallel random access machine (PRAM) is the most commonly used generalpurpose machine model for describing parallel computations.Unfortunately the PRAM model is not physically realizable, since on large machines a parallel shared memory access can only be accomplished at the cost of a significant time delay. A number of PRAM simulation algorithms are known. The algorithms allow execution of PRAM programs on more realistic parallel machines. We study the randomized simulation of an exclusive read, exclusive write (EREW) PRAM on a module parallel computer (MPC). The simulation is based on utilizing universal hashing. The optimally efficient simulation involving parallel slackness is also investigated. The results of our experiments performed on the MPC built upon IMS T9000 transputers throw some light on the question whether using the PRAM model in parallel computations is practically viable given the present state of transputer technology.

Pregrammars Versus Submonoids
Jan Ostravsky
pages 337-343

Prelanguages and pregrammars introduced in [8] present a generalization of languages and pure grammars. Relation of domination and double domination may be easily transferred from languages to prelanguages. In the present paper submonoids of a commutative monoid are characterized by means of their relations of domination; subgroups of a commutative group are characterized by means of their relations of double domination. The submonoid generated by a subset of a commutative monoid is constructed using
a suitable pregrammar.
The Modified Oja-RLS Algorithm, Stochastic Convergence Analysis and Application for Image Compression
Władysław Skarbek, Adam Pietrowcew and Radosław Sikora
pages 345-365

The results of theoretical analysis for stochastic convergence of the modified Oja-RLS learning rule are presented. The rule is used to find Karhunen Loeve Transform. Based on this algorithm, an image compression scheme is developed by combining approximated 2D KLT transform and JPEG standard quantization and entropy coding stages. Though 2D KLT transform is of higher complexity than 2D DCT,
the resulting PSNR quality of reconstructed images is better even by 2.
Simple and Minimal Ground Term Equation Systems
Sandor Vagvolgyi
pages 367-413

A ground term equation system (gtes for short) E is simple if there is no gtes E' equivalent to E consisting of less equations than E has. Moreover, a gtes E is minimal if for each equation e in E, the congruence generated by E-{e} is a proper subset of the congruence generated by E. Given a reduced ground term rewriting system R, we describe all simple gtes' E and minimal gtes' F equivalent to R. We show that for a reduced ground term rewriting system R, it is decidable whether or not there exist infinitely many simple (minimal) gtes' equivalent to R. Finally, we show that for a reduced ground term rewriting system R, and a gtes E, it is decidable if there is a simple gtes F equivalent to R such that Euis a subset of F.