FI,  Abstracts vol. 61

62(1)  2004


  1. Preface i-iii

    Continuous Time Paradigms in Logic and Automata

    In the last 15 years, research in Computer Science has involved many paradigms in which continuous time appears whether in a pure way or in cooperation with discrete time. In particular, this is evident in subjects concerning Automata and Logic. This issue of FI consists of four papers dedicated to such subjects. The papers will be referred to below as [HR], [S], [PRT], [T] (the initials of the authors). [HR] and [S] are about continuous-time logics, whereas in [T] and [PRT] the focus is on automata.

    In [HR] the concern is about Monadic Logics of Order (MLO) and their relationship to Temporal Logics. For discrete time, decidability of Second Order Monadic Logic (SOML) follows from the connection between SOML and automata theory. It is well known that SOML covers numerous temporal logics (TL). Ultimately, these TL may be considered as syntactically sugared versions of SOML fragments. In [HR] further facts of this kind are established for continuous time. However, in this case, instead of traditional automata-theoretic techniques one needs to use properly general theorems from logic.

    The logic framework developed in [S] is based on First Order Timed Logic (FOTL), that allows functions and predicates with more than one argument; moreover, it allows also some arithmetics. This makes the logic expressive enough to represent, more or less directly, continuous-time properties of distributed algorithms. But, on the other hand, it makes the logic undecidable. The fundamental observation that, nevertheless, permits the efficient use this logic for verification is as follows: the underlying theories of continuous time (e.g. the theory of real addition, Tarski algebra, etc.) are decidable or have much better complexity than the corresponding theories of discrete time. Interesting decidable classes of the verification problem are based on appropriate properties of FOTL.

    The companion papers [T] and [PRT] draw their initial motivation from the literature on Hybrid Automata, Circuits and related control problems. Concrete problems about circuits (feedback reliability, completeness) and control (sample-and-hold architectures in continuous time) are also the subject of [T] and [PRT]. Yet, a more general contribution is the development of a conceptual framework that allows one to highlight the genuine distinctions and similarities between the discrete-time and continuous-time tracks.

    There is a growing feeling in the community that the literature on these subjects, as well on the related logics, is plagued by a Babel of models, constructs and formalisms with an amazing discord of terminology and notation. Further models and formalisms are engendered, and it is not clear where to stop. Hence, appeals like:

    1. ``look back to sort out what has been accomplished and what needs to be done... by surveying logic-based and automata-based real-time formalisms and putting them into a perspective" (R. Alur and T.Henzinger).

    2. ``...isolate the right concepts, ... formulate the right models, and discard many others, that do not capture the reality we want to understand..."(J. Hartmanis).

    The analysis of such formalisms and systems is not the goal of [S]; here the control systems under consideration are reduced to rather primitive ones by declaring the relevant properties in logic specifications. Accordingly, [S] confines itself to the following informal remark: an algorithm interacting with a continuous-time device is, usually, called a hybrid automaton.

    On the other hand, [HR], [T] and [PRT] are strongly committed to the analysis in depth of the various continuous-time paradigms and to their robust conceptual integration in mainstream Automata Theory and Logic. These papers come to the following conclusions about misconceptions in the previously suggested models and logics:

    (i). The standard continuous-time model for logic was ignored as a yardstick; instead, different kinds of sequences of continuous-time bits were used ([HR]).

    (ii). Input/output behavior of automata was ignored in favor of generating devices ([T]).

    More details and reflections follow:

    [HR]: When it came to continuous time most of the researchers decided to abandon the natural model of the real line in favor of discrete models in which the elements of the sequence were decorated by some information concerning the real line. This may have been an attempt to pursue the connection with automata theory since automata were traditionally associated with sequences. This was the main cause in the rejection of the classical model. It complicated the subsequent research. The choice of the temporal logic became an arbitrary decision which was no longer backed up by the expressive power of classical logic. A host of different formalisms was introduced, as well as an astonishing variety of pairs ``model - logic". This work never converged to an accepted model; models and formalisms continued to proliferate.

    [T]: Functions (in particular, input/output behavior of automata) are more fundamental than sets (say, languages accepted by automata). In particular, the restriction to language - theoretic formulations hides issues that are crucial for proper handing of circuits and hybrids. Surprisingly, it has been left unobserved that some flaws in the conceptual decisions concerning continuous time are identifiable already at the level of discrete-automata theory.

    Editorial and historical comments. Sometimes, slightly different notation and terminology are used in the papers. This is visible especially in the companion papers [PRT] and [T] that have much in common but were written at different times. It seemed too burdensome to impose unified standards and to require the respective revisions. Hopefully, the reader will easily overcome this lack of uniformity due to appropriate footnotes and mutual references.

  2. Logics for Real Time: Decidability and Complexity
    Yoram Hirshfeld and Alexander Rabinovich 1-28

    Over the last fifteen years formalisms for reasoning about metric properties of computations were suggested and discussed. First as extensions of temporal logic, ignoring the framework of classical predicate logic, and then, with the authors' work, within the framework of monadic logic of order. Here we survey our work on metric logic comparing it to the previous work in the field. We define a quantitative temporal logic that is based on a simple modality within the framework of monadic predicate Logic. Its canonical model is the real line (and not an w-sequence of some type). It can be interpreted either by behaviors with finite variability or by unrestricted behaviors. For finite variability models it is as expressive as any logic suggested in the literature. For unrestricted behaviors our treatment is new. In both cases we prove decidability and complexity bounds using general theorems from logic (and not from automata theory).

  3. A Logic Framework for Verification of Timed Algorithms
    Anatol Slissenko 29-67

    This paper is a survey of research of my colleagues and myself aimed at developing a comprehensive logical framework for the verification of real-time distributed systems. The framework is based on predicate logics with explicit time. To choose such a logic we pursue two goals: first, to make formalization of verification problems rather direct, without unjustified simplifications, and second, to have a logic which permits to describe decidable classes of the verifications problem covering the particular problems we are interested in. Notice that our intention is not to introduce new specification languages, but work directly with those of the user.

    In this paper we describe First Order Timed Logic (FOTL) that is sufficient to express the main part of verification of systems without uncertainty. The time is continuous (the formalism work as well for discrete time - in our context this case is less interesting and less efficient from algorithmic viewpoint). We give examples of problems that can be treated, describe how to represent runs of programs in FOTL, introduce decidable classes, discuss aspects of practical efficiency. We conclude with open questions.

  4. Understanding Basic Automata Theory in the Continuous Time Setting
    B. A. Trakhtenbrot 69-121

    Paradigms, in which continuous time is involved in cooperation with, or instead of, discrete time appear now in different areas related to automata, logic and interaction. Unfortunately, they are accompanied by a plethora of definitions, terminology and notation, which is not free of ad-hoc and ambiguous decisions. The overuse of definitions from scratch of intricate notions without a previous, explicit core of basic generic notions engenders further models and formalisms, and it is not clear where to stop. Hence (quoting J.Hartmanis), the challenge ``to isolate the right concepts, to formulate the right models, and to discard many others, that do not capture the reality we want to understand...".

    We undertake this challenge wrt some automata-theoretic concepts and issues that appear in the literature on continuous-time circuits and hybrid automata, by keeping to the following guidelines:

    1. Building on Basic Automata Theory.

    2. Coherence with original or potential discrete-time paradigms, whose continuous-time analogs and/or mutants we would like to understand.

    3. Functions, notably input/output behavior of devices, should not be ignored in favor of sets (languages) accepted by them.

    The paper outlines the approach which emerged in previous research [PRT, RT, T3, T4, R] and in teaching experience [T0, T2]. As an illustration we offer a precise explanation of the evasive relationship between hybrid automata, constrained automata and control circuits.

     

  5. Synchronous Circuits over Continuous Time: Feedback Reliability and Completeness
    D. Pardo, A. Rabinovich and B.A. Trakhtenbrot 123-137

    To what mathematical models do digital computer circuits belong? In particular:

    (i) (Feedback reliability.) Which cyclic circuits should be accepted? In other words, under which conditions is causally faithful the propagation of signals along closed cycles of the circuit?

    (ii) (Comparative power and completeness.) What are the appropriate primitives upon which circuits may be (or should be) assembled?

    There are well-known answers to these questions for circuits operating in discrete time, and they point on the exclusive role of the unit-delay primitive. For example:

    (i) If every cycle in the circuit N passes through a delay, then N is feedback reliable.

    (ii) Every finite-memory operator F is implementable in a circuit over unit-delay and pointwise boolean gates.

    In what form, if any, can such phenomena and results be extended to circuits operating in continuous time? This is the main problem considered (and, hopefully, solved to some extent) in this paper.

    In order to tackle the problems one needs more insight into specific properties of continuous time signals and operators that are not visible at discrete time.


62(2) 2004


  1. Preface i-ii

    The Second Special Issue on Application of Concurrency to System Design

    The articles in this special issue of Fundamenta Informaticae are revised versions of selected papers presented in the Third International Conference on Application of Concurrency to System Design (ACSD'03) held in Guimarães, Portugal, 18-20 June, 2003. The first conference in the series was held in Aizu-Wakamatsu, Japan, March 1998, the second in Newcastle upon Tyne, U.K., June 2001. The journal versions of six selected papers from ACSD'01 were published in Fundamenta Informaticae, Vol. 50, Number 2, April 2002. The five papers have been chosen from 22 contributions accepted for presentation at ACSD'03, following their additional evaluation and editorial treatment. Like its predecessors, the Guimarães Conference was organized to provide a forum for disseminating advanced research results on theory, algorithms, and case studies arising in the design of concurrent systems. The chosen articles cover complexity issues, asynchronous circuits, reactive syatems, scheduling, refinement and synthesis problems. The order of contributions is alphabetical. The first article by Y. Bontemps, P.-Y. Schobbens and C. Löding is devoted to synthesis of open reactive systems. They start with scenario-based specifications and propose Live Sequence Charts with a new, game-based, semantics to model interactions between the system and its environment. In the second article, J. Cortadella, A. Kondratyev, L. Lavagno, A. Taubin, Y. Watanabe address the problem of quasi-static scheduling for concurrent architectures. Their paper presents a synthesis approach for reactive syatems that aims at minimizing the overhead introduced by the operating system and the interaction among the concurrent tasks, while considering multiple concurrent execution resources. In the third article, J. Esparza provides a surprising polynomial-time algoritnm for checking consitency of free-choice singal transition graphs. The fourth article by V. Khomenko, M. Koutny and A. Yakovlev addresses the problem of detecting state encoding conflicts in Signal Transition Graphs. The problem is proven to be NP-complete. The authors propose an algorithm based on the Boolean Satisfiability (SAT) approach. The SAT problem is of course also NP-complete, but there exist many heuristic efficient algorithms for SAT working very well for äverage" case. In the fifth article and the last, J.-P. Talpin, P. Le Gueric, S. K. Shukla, F. Doucet, and R. Gupta proposes a new approach to formal refinement-checking. They apply the concept of multi-clock synchrony, and demonstrate the effectiveness of the approach by experimental and comparative study of a SPECC programming example. I am very grateful to the authors for submitting their papers and to the referees for their useful criticism.
     

    Ryszard Janicki
    Department of Computing and Software
    McMaster University
    Hamilton, Ontatio
    Canada L8S 4K1
    janicki@mcmaster.ca

     

  2. Synthesis of Open Reactive Systems from Scenario-Based Specifications
    Yves Bontemps, Pierre-Yves Schobbens and Christof Löding 139-169

    We propose here Live Sequence Charts with a new, game-based semantics to model interactions between the system and its environment. For constructing programs automatically, we give an algorithm to synthesize either a strategy for the system ensuring that the specification is respected, or, if the specification is unimplementable, a strategy for the environment forcing the system to fail. We introduce the concept of mercifulness, a desirable property of the synthesized program. We give a polynomial time algorithm for synthesizing merciful winning strategies.

     

  3. Quasi-static Scheduling for Concurrent Architectures
    Jordi Cortadella, Alex Kondratyev, Luciano Lavagno, Alexander Taubin and Yosinori Watanabe 171-196

    This paper presents a synthesis approach for reactive systems that aims at minimizing the overhead introduced by the operating system and the interaction among the concurrent tasks, while considering multiple concurrent execution resources. A formal model based on the notion of scheduling of Petri nets is used to perform the synthesis. We show how the notion of projections of a schedule for the complete system onto the components implemented on separate resources is essential to define the correctness of the partitioned schedule.

     

  4. A Polynomial-Time Algorithm for Checking Consistency of Free-Choice Signal Transition Graphs
    Javier Esparza 197-220

    Signal Transition Graphs (STGs) are one of the most popular models for the specification of asynchronous circuits. A STG can be implemented if it admits a so-called consistent and complete binary encoding. Deciding this is EXPSPACE-hard for arbitrary STGs, and so a lot of attention has been devoted to the subclass of free-choice STGs, which offers a good compromise between expressive power and analizability. In the last years, polynomial time synthesis techniques have been developed for free-choice STGs, but they assume that the STG has a consistent binary encoding. This paper presents the first polynomial algorithm for checking consistency.

     

  5. Detecting State Encoding Conflicts in STG Unfoldings Using SAT
    Victor Khomenko, Maciej Koutny and Alex Yakovlev 221-241

    The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is that of identifying whether an STG satisfies the Complete State Coding (CSC) requirement (which states that semantically different reachable states must have different binary encodings), and, if necessary, modifying the STG (by, e.g., inserting new signals helping to trace the current state) to meet this requirement. This is usually done using reachability graphs.

    In this paper, we avoid constructing the reachability graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for detection of CSC conflicts based on the Boolean Satisfiability (SAT) approach. Following the basic formulation of the state encoding conflict relationship, we present some problem-specific optimization rules. Experimental results show that this technique leads not only to huge memory savings when compared to the CSC conflicts detection methods based on reachability graphs, but also to significant speedups in many cases.

     

  6. Formal Refinement Checking in a System-level Design Methodology
    Jean-Pierre Talpin, Paul Le Guernic, Sandeep Kumar Shukla, Frédéric Doucet and Rajesh Gupta 243-273

    Rising complexity, increasing performance requirements, and shortening time-to-market demands necessitate newer design paradigms for embedded system design. Such newer design methodologies require raising the level of abstraction for design entry, reuse of intellectual property blocks as virtual components, refinement based design, and formal verification to prove correctness of refinement steps. The problem of combining various components from different designers and companies, designed at different levels of abstraction, and embodying heterogeneous models of computation is a difficult challenge for the designer community today. Moreover, one of the gating factors for widespread adoption of the system-level design paradigm is the lack of formal models, method and tools to support refinement. In the absence of provably correct and adequate behavioral synthesis techniques, the refinement of a system-level description towards its implementation is primarily a manual process. Furthermore, proving that the implementation preserves the properties of the higher system-level design-abstraction is an outstanding problem. In this paper, we address these issues and define a formal refinement-checking methodology for system-level design. Our methodology is based on a polychronous model of computation of the multi-clocked synchronous formalism Signal. This formalism is implemented in the Polychrony workbench. We demonstrate the effectiveness of our approach by the experimental case study of a SpecC modeling example. First, we define a technique to systematically model SpecC programs in the Signal formalism. Second, we define a methodology to compare system-level models of SpecC programs and to validate behavioral equivalence relations between these models at different levels of abstraction. Although we use SpecC modeling examples to illustrate our technique, our methodology is generic and language-independent and the model that supports it conceptually minimal by offering a scalable notion and a flexible degree of abstraction.

62(3-4)~~2004

62(3-4)  2004


  1. An Adaptive Steganographic Scheme for Color Images
    Chin-Chen Chang, Piyu Tsai and Min-Hui Lin 275-289

    In this paper, a new palette-based image steganography is proposed. Palette-based images such as GIF files have been widely used on the Internet and web pages such that all browsers can recognize them. Palette-based images can be used as good carriers for transmitting secret messages. In this scheme, the Least Significant Bits (LSBs) of the palette-based image are utilized in order to hide the secret message by using the computational information hiding technique. The adaptive hiding capacity can be computed according to different sizes of the embedding block.

    Experimental results also show that existing artifacts in the traditional LSB-based method are unnoticeable. The number of modification pixels in the embedding process is decreased, while good stego-image quality is maintained, and the cover image is left unblemished by camouflaged information. Furthermore, the feature of adaptive hiding capacity provides the possibility of protecting different sizes of embedded secret messages.

  2. A Timed Extension for ALTARICA
    Franck Cassez, Claire Pagetti and Olivier Roux 291-332

    In this paper we present a timed extension of the AltaRica formalism. Following previous works, we first extend the semantics of AltaRicawith time and define timed components and timed nodes. Moreover we lift the priority features of AltaRicato the timed case. We obtain a timed version of AltaRica, called Timed AltaRica. Finally we give a translation of a Timed AltaRicaspecification into a usual timed automaton. These are the semantic foundations of a high-level hierarchical language for the specification of timed systems.

  3. An w-Power of a Finitary Language Which is a Borel Set of Infinite Rank
    Olivier Finkel 333-342

    w-powers of finitary languages are w-languages s in the form Vw, where V is a finitary language over a finite alphabet S. Since the set Sw of infinite words over S can be equipped with the usual Cantor topology, the question of the topological complexity of w-powers naturally arises and has been raised by Niwinski [13], by Simonnet [15], and by Staiger [18]. It has been proved in [4] that for each integer n ³ 1, there exist some w-powers of context free languages which are Pn0-complete Borel sets, and in [5] that there exists a context free language L such that Lw is analytic but not Borel. But the question was still open whether there exists a finitary language V such that Vw is a Borel set of infinite rank.
    We answer this question in this paper, giving an example of a finitary language whose w-power is Borel of infinite rank.

  4. Query compilation under the disjunctive well-founded semantics
    Chris A. Johnson 343-368

    A top-down method is presented for compiling queries in unstratified propositional disjunctive deductive databases under the disjunctive well-founded semantics. Compilation entails the construction of a set of compilation trees, and the run-time processing of the compiled query then amounts to checking that some such tree can be extended within the extensional database to yield a tree that encapsulates a proof of the original query. Issues surrounding the extension of our techniques to the first order level are discussed.

  5. Approximation Algorithms for MAX-BISECTION on Low Degree Regular Graphs
    Marek Karpinski, Miroslaw Kowaluk and Andrzej Lingas 369-375

    The max-bisection problem is to find a partition of the vertices of a graph into two equal size subsets that maximizes the number of edges with endpoints in both subsets.

    We obtain new improved approximation ratios for the max-bisection problem on the low degree k-regular graphs for 3 £ k £ 8, by deriving some improved transformations from a maximum cut into a maximum bisection. In the case of three regular graphs we obtain an approximation ratio of 0.854, and in the case of four and five regular graphs, approximation ratios of 0.805, and 0.812, respectively.

  6. The Compactness of Belief Revision and Update Operators
    Paolo Liberatore and Marco Schaerf 377-393

    A propositional knowledge base can be seen as a compact representation of a set of models. When a knowledge base T is updated with a formula P, the resulting set of models can be represented in two ways: either by a theory T¢ that is equivalent to T*P or by the pair \l T,P \r. The second representation can be super-polinomially more compact than the first. In this paper, we prove that the compactness of this representation depends on the specific semantics of *, , Winslett's semantics is more compact than Ginsberg's.

  7. Optimal Unification of Infinite Sets of Types
    Jacek Marciniec 395-407

    In this paper we focus on the properties of infinite sets of types that have finite substitutional images. Since the number of such images may be infinite, we provide the way of its reduction. Having this done, we apply the new methods in the field of learnability of classical categorial grammars.

  8. A Rough Set Theoretic Approach to Clustering
    Supriya Kumar De 409-417

    In this paper, cluster analysis based on fuzzy relations is investigated. This paper starts with fuzzy proximity relations and cluster analysis based on fuzzy proximity relation is performed by using rough approximation. A clustering algorithm has been proposed and explained with an example.