Behavioral Logics

From FSL

Jump to: navigation, search

Contents

[edit] Behavioral Equivalence and Logic

The notion of behavioral equivalence arises naturally in the theory of systems. The abstract identity of a system is established by its behavior, and not by its isomorphism class. Many-sorted algebras model systems in a direct and natural way, with operations representing (parameterized) transitions.
Behavioral logic is an extension of many-sorted algebra that emphasizes the view of algebras as systems by establishing the distinction between hidden and visible sorts. Elements of hidden sorts are the states of the system, and those of visible sorts are the given data. While data is directly accessible and fully transparent to the user, states may only be accessed by means of experiments. In this algebraic setting, an experiment is simply a context, i.e., a term with a hole in it, of visible sort. Two states are behaviorally equivalent if no experiment can distinguish between them, i.e., if they yield the same result under any chain of operation applications that yields observable result.
Behavioral equivalence turns out to be an algebraic congruence, the largest one that does not identify any non-equal data. Factorizing the original algebra to its behavioral equivalence yields an algebraic notion of abstract behavior of a system. The original algebra may be thought of as an implementation of this abstract behavior.
Behavioral equivalence induces an appropriate notion of satisfaction: an algebra is required to satisfy an equation behaviorally rather than strictly. In case no non-congruent (i.e., implementation-specific) operations occur in the algebra, behavioral satisfaction should coincide with strict satisfaction in the abstract-behavior quotient of the algebra.


[edit] Automating Coinduction

Coinduction is the main coalgebraic technique for proving properties about infinite systems and data structures, such as streams. By capturing many coalgebraic situations of interest, behavioral logic offers a completely formalized setting for reasoning about them. Therefore any deductive system for behavioral logic would yield a coalgebraic theorem prover.
Due to its capability to reason about almost arbitrary infinite structures, behavioral logic is not recursively axiomatizable (or, equivalently, not recursively enumerable). This is not surprising, since even the simple case of streams turns out to be non-RE (cite rosu-streams). Searching for deductive systems as powerful as possible was a leading concern of Grigore's Ph.D. thesis (cite) (thesis which reflected work jointly with his advisor Joseph Goguen). The Circular Coinduction (CC) deduction rule, and its implementation by the CC algorithm, offer a heuristic for performing coinduction while at the same time searching for an appropriate coinductive hypothesis. Its circular aspect comes from the fact that it uses a sentence as hypothesis in a deduction that might end up proving itself; this is perfectly sound in a coinductive setting, where repetition of a certain goal throughout a proof yields its success, as it survived all attempts of disproving it. A behavioral specification language in the OBJ family (cite), BOBJ, implements the CC algorithm, shown to work well on many examples.
Inevitably, CC crashes on some examples, especially on those involving case analysis or induction in combination with coinduction. The CC technique was refined and improved in a series of papers (cite), and was applied to regular expressions (cite) and to monitoring temporal logic formulae (cite). We are currently working at a circular-coinductive theorem prover called CIRC that aims at balancing coinduction with induction and other techniques. The main idea is to take advantage also of the situations where a fully-automated version of CC would crash. Indeed, is one was to stop an infinite loop where the CC algorithm has ventured, one might find plenty of potentially useful, but inaccessible, information. We chose to run the CC deduction rule more interactively, on a by need bases; this way, it can be offered assistance, e.g., by means of launching an inner induction.

[edit] Behavioral Logics as Institutions

Institutions, introduced by Goguen and Burstall in the eighties, are abstract model-theoretic notions of logical systems. Most logics in current use are particular cases of institutions.
Various versions of behavioral logics were organized as institutions in various ways. While proving a logic to form an institution is an important test for the logic and a useful thing to do (thanks to this more structural view yielding theorems-for-free and such), we believe that the real test of behavioral logic comes from testing the bases of its originating construction itself. The paper (cite) proves that the notions of behavioral satisfaction and equivalence are logic-independent, in that they can be defined on top of any logical system.

[edit] Behavioral Logic and Coalgebra

Coalgebra theory was developed as a framework for describing and proving properties about infinite systems. Its techniques - coinduction and corecursion - are somehow dual to the classical induction and recursion. This duality exists however more in spirit than in form, since algebra and coalgebra, though categorically dual, are not inter-reducible as the category of sets (which works as support for both) is not self dual.
In coalgebra, a desired infinite system is described as the final object of an appropriate "unfolding" functor on Set. The system represented by this final object, as naturally isomorphic to its unfolding, is fully abstract in the sense that "it is what it does" (cite rutten-turi).
There is a tight connection between coalgebra and behavioral logic. Roughly, both frameworks deal with systems and their behaviors; but while the former identifies a universal and fully-abstract system comprising all possible behaviors, the latter approaches systems more locally, and inquires each system for the properties of its particular abstract behavior. The intersection of the two approaches is given by situations from behavioral logic (specifications having monadic cobases), where models can be regarded as coalgebras for a certain functor.
Behavioral algebraic specifications are more flexible than coalgebraic definitions in that they do not require the operations to have certain ranks or to be fully defined. This flexibility of behavioral logic, which naturally allows for underspecification, is particularly suitable for theorem proving purposes. Moreover, due to its lax notion of model, behavioral logic can handle relationships between implementations and desired systems.
On the other hand, the coalgebraic definitional style can more readily express nondeterminism, since set-theoretic constructs such as direct sums and powersets may be freely used in this rigorous but informal mathematical setting. We believe that behavioral logic techniques could be appropriately adapted for handling nondeterminism too. A demonstration of modeling a restricted form of nondeterminism has already been made in (cite gogu/lin). We are currently working on combining the behavioral and rewriting logic methodologies in order to address the issue of nondeterminism in its full generality.


[edit] Publications with Abstracts

Circular Coinduction with Special Contexts
Dorel Lucanu and Grigore Rosu
Image:New.gif ICFEM'09, to appear in LNCS. 2009
Abstract. Coinductive proofs of behavioral equivalence often require human ingenuity, in that one is expected to provide a good relation extending one's goal with additional lemmas, making automation of coinduction a challenging problem. Since behavioral satisfaction is a \Pi_2^0-hard problem, one can only expect techniques and methods that approximate the behavioral equivalence. Circular coinduction is an automated technique to prove behavioral equivalence by systematically exploring the behaviors of the property to prove: if all behaviors are circular then the property holds. Empirical evidence shows that one of the major reasons for which circular coinduction does not terminate in practice is that the circular behaviors may be guarded by a context. However, not all contexts are safe. This paper proposes a large class of contexts which are safe guards for circular behaviors, called special contexts, and extends circular coinduction appropriately. The resulting technique has been implemented in the CIRC prover and experiments show that the new technique can prove many interesting behavioral properties fully automatically.
PDF, ICFEM'09, BIB
Circular Coinduction: A Proof Theoretical Foundation
Grigore Rosu and Dorel Lucanu
CALCO'09, LNCS 5728, pp 127-144. 2009
Abstract. Several algorithmic variants of circular coinduction have been proposed and implemented during the last decade, but a proof theoretical foundation of circular coinduction in its full generality is still missing. This paper gives a three-rule proof system that can be used to formally derive circular coinductive proofs. This three-rule system is proved behaviorally sound and is exemplified by proving several properties of infinite streams. Algorithmic variants of circular coinduction now become heuristics to search for proof derivations using the three rules.
LNCS, CALCO'09, DBLP, BIB
CIRC: A Circular Coinductive Prover
Dorel Lucanu and Grigore Rosu
CALCO'07, LNCS 4624, pp 372-378. 2007
Abstract. CIRC is an automated circular coinductive prover implemented as an extension of Maude. The circular coinductive technique that forms the core of CIRC is discussed, together with a high-level implementation using metalevel capabilities of rewriting logic. To reflect the strength of CIRC in automatically proving behavioral properties, an example defining and proving properties about infinite streams of infinite binary trees is shown. CIRC also provides limited support for automated inductive proving, which can be used in combination with coinduction.
PDF, CIRC webpage, CALCO'07, BIB
Equality of Streams is a Pi_2^0-Complete Problem
Grigore Rosu
ICFP'06, ACM, 2006
Abstract. This paper gives a precise characterization for the complexity of the problem of proving equal two streams defined with a finite number of equations: \Pi_2^0. Since the \Pi_2^0 class includes properly both the recursively enumerable and the co-recursively enumerable classes, this result implies that neither the set of pairs of equal streams nor the set of pairs of unequal streams is recursively enumerable. Consequently, one can find no algorithm for determining equality of streams, as well as no algorithm for determining inequality of streams. In particular, there is no complete proof system for equality of streams and no complete system for inequality of streams.
PDF, ICFP'06 Slides, ACM, ICFP'06, BIB
Behavioral Extensions of Institutions
Andrei Popescu and Grigore Rosu
CALCO'05, LNCS 3629, pp. 331-347. 2005
Abstract. We show that any institution \mathcal{I} satisfying some reasonable conditions can be transformed into another institution, {\mathcal{I}}_{beh}. This transformation captures formally and abstractly the intuitions of adding support for behavioral equivalence and reasoning to an existing, particular algebraic framework. We call our transformation an "extension" because {\mathcal I}_{beh} has the same sentences as \mathcal I and because its entailment relation includes that of \mathcal I. Many properties of behavioral equivalence in concrete hidden logics follow as special cases of corresponding institutional results. As expected, the presented constructions and results can be instantiated to other logics satisfying our requirements as well, thus leading to novel behavioral logics, such as partial, infinitary, or second-order ones, that have the desired properties.
PDF, CALCO'05 Slides, LNCS , CALCO '05, DBLP, BIB
Behavioral Abstraction is Hiding Information
Grigore Rosu
J. of TCS, Volume 327(1-2), pp 197-221. 2004
Abstract. We show that for any behavioral Σ-specification ~{B} there is an ordinary algebraic specification \tilde{B} over a larger signature, such that a model behaviorally satisfies ~B iff it satisfies, in the ordinary sense, the Σ-theorems of \tilde{B}. The idea is to add machinery for contexts and experiments (sorts, operations and equations), use it, and then hide it. We develop a procedure, called unhiding, which takes a finite ~B and produces a finite \tilde{B}. The practical aspect of this procedure is that one can use any standard equational inductive theorem prover to derive behavioral theorems, even if neither equational reasoning nor induction is sound for behavioral satisfaction.
PDF, J.TCS, BIB
Inductive Behavioral Proofs by Unhiding
Grigore Rosu
CMCS'03, ENTCS 82(1). 2003
Abstract. We show that for any behavioral Σ-specification ~B there is an ordinary algebraic specification \tilde{B} over a larger signature, such that a model behaviorally satisfies ~B iff it satisfies, in the ordinary sense, the Σ-theorems of \tilde{B}. The idea is to add machinery for contexts and experiments (sorts, operations and equations), use it, and then hide it. We develop a procedure, called unhiding, which takes a finite ~B and produces a finite \tilde{B}. The practical aspect of this procedure is that one can use any standard equational inductive theorem prover to derive behavioral theorems, even if neither equational reasoning nor induction is sound for behavioral satisfaction.
PDF, ENTCS, CMCS'03, Experiments, DBLP, BIB
Hidden Logic
Grigore Rosu
PhD Thesis, University of California at San Diego
Abstract. Cleverly designed software often fails to satisfy its requirements strictly, but instead satisfies them behaviorally, in the sense that they appear to be satisfied under every experiment that can be performed on the system. It is therefore becoming increasingly important to develop powerful techniques for behavioral specification and verification of systems, especially in the design stage, where most of the errors appear.

The general context of this thesis is formal methods for software and/or hardware development. We will present a promising new logic together with a language to support it, with applications to various branches of computer science, especially to the specification and automated verification of object-oriented and concurrent systems.

The thesis can be roughly divided into three major parts. The first is dedicated to presenting hidden logic in an easy going and intuitive way, with many examples, to developing sound inference rules, including a series of non-trivial coinduction rules, and to presenting a specification language in the OBJ family, called BOBJ, supporting hidden logic and reasoning. The second part is on automation of behavioral reasoning; more precisely, it introduces the techniques called behavioral rewriting, behavioral coinductive rewriting and circular coinductive rewriting, which are implemented in BOBJ. The third and the last part relates to more theoretical aspects of the logic, including relationships with other formalisms and theories, such as information hiding, coalgebra, institutions, Birkhoff-like axiomatizability, and incompleteness.
PDF, Thesis@UCSD, BIB


[edit] Related External Links

[edit] Behavioral and Hidden Logics

[edit] Others

Retrieved from "http://fsl.cs.uiuc.edu/index.php/Behavioral_Logics"
Views
Personal tools