Generating Model Checkers from Algebraic Specifications

There is a great deal of research aimed toward the development of temporal logics and model checking algorithms which can be used to verify properties of systems. In this paper, we present a methodology and supporting tools which allow researchers and practitioners to automatically generate model checking algorithms for temporal logics from algebraic specifications. These tools are extensions of algebraic compiler generation tools and are used to specify model checkers as mappings of the form , where L _s is a temporal logic source language and L _t is a target language representing sets of states of a model M, such that . The algebraic specifications for a model checker define the logic source language, the target language representing sets of states in a model, and the embedding of the source language into the target language. Since users can modify and extend existing specifications or write original specifications, new model checking algorithms for new temporal logics can be easily and quickly developed; this allows the user more time to experiment with the logic and its model checking algorithm instead of developing its implementation. Here we show how this algebraic framework can be used to specify model checking algorithms for CTL, a real-time CTL, CTL*, and a custom extension called CTL ^e that makes use of propositions labeling the edges as well as the nodes of a model. We also show how the target language can be changed to a language of binary decision diagrams to generate symbolic model checkers from algebraic specifications.     

Presenting functors on many-sorted varieties and applications

This paper studies several applications of the notion of a presentation of a functor by operations and equations. We show that the technically straightforward generalisation of this notion from the one-sorted to the many-sorted case has several interesting consequences. First, it can be applied to give equational logic for the binding algebras modelling abstract syntax. Second, it provides a categorical approach to algebraic semantics of first-order logic. Third, this notion links the uniform treatment of logics for coalgebras of an arbitrary type T with concrete syntax and proof systems. Analysing the many-sorted case is essential for modular completeness proofs of coalgebraic logics.     

Bases for closed sets of implicants and implicates in temporal logic

Prime implicates and implicants are used in several areas of Artificial Intelligence. However, their calculation is not always an easy task. Nevertheless, it is important to remark the distinction between (i) computing the prime implicates and implicants and (ii) using the information they contain. In this paper, we present a way in which (ii) can be done without actually doing (i) by limiting prime implicants and implicates management to unitary implicants and implicates. Besides, we outline how the use of this technique is particularly relevant in the field of automated deduction in temporal logics. The information contained in temporal implicates and implicants can be used to design transformations of temporal formulae able to increase the power of automated deduction techniques for temporal logics. Particularly, we have developed a theory for unitary temporal implicates and implicants that can be more efficiently computed than prime implicants, while still providing the information needed to design this kind of transformations. The theory we have developed in this paper is easily extensible to cover different types of temporal logics, and is integrable in different automated deduction methods for these temporal logics. Received: 14 May 1999 / 22 March 2002     

一类扩展的动态描述逻辑

作为描述逻辑的扩展,动态描述逻辑为语义Web服务的建模和推理提供了一种有效途径.在将语义Web服务建模为动作之后,动态描述逻辑从动作执行结果的角度提供了丰富的推理机制,但对于动作的执行过程却不能加以处理.借鉴Pratt关于命题动态逻辑的相关研究,一方面,对动态描述逻辑中动作的语义重新进行定义,将每个动作解释为由关于可能世界的序列组成的集合;另一方面,在动态描述逻辑中引入动作过程断言,用来对动作的执行过程加以刻画.在此基础上提出一类扩展的动态描述逻辑EDDL(X),其中的X表示从ALC(attributive language with complements)到SHOIN(D)等具有不同描述能力的描述逻辑.以X为描述逻辑ALCQO(attributive language with complements,qualified number restrictions and nominals)的情况为例,给出了EDDL(ALCQO)的表判定算法,并证明了算法的可终止性、可靠性和完备性.EDDL(X)可以从动作执行过程和动作执行结果两个方面对动作进行全面的刻画和推理,为语义Web服务的建模和推理提供了进一步的逻辑支持.     

Epistemic logic and logical omniscience: A survey

This survey brings together a collection of epistemic logics and discusses their approaches in alleviating the logical omniscience problem. Of particular note is the logic of implicit and explicit belief. Explicit belief refers to information actively held by an agent, while implicit belief refers to the logical consequence of explicit belief. Ramifications of Levesque's logic include nonstandard epistemic logic and the logics of awareness and local reasoning. Models of nonstandard epistemic logic are defined with respect to nonstandard proportional logic to weaken its semantics. In the logic of awareness, an agent can only believe a concept that it is aware of. Closely related to awareness are S-1 and S-3 epistemic operators which can be used to model skeptical and credulous agents. The logic of local reasoning provides a semantics for representing the fact that agents can have different clusters of beliefs which may contradict each other. Other variations include epistemic structures which are generalizations of the logic of local reasoning and fusion epistemic models which provide an account that agents can combine information conjunctively or disjunctively. Another closely related approach is the logic of explicit propostions which captures the insight that agents can hold beliefs independently without putting them together. © 1997 John Wiley & Sons, Inc.     

An Infinite Hierarchy of Temporal Logics over Branching Time

Many temporal logics have been suggested as branching time specification formalisms during the past 20 years. These logics were compared against each other for their expressive power, model checking complexity, and succinctness. Yet, unlike the case for linear time logics, no canonical temporal logic of branching time was agreed upon. We offer an explanation for the multiplicity of temporal logics over branching time and provide an objective quantified yardstick to measure these logics. We define an infinite hierarchy BTL_k of temporal logics and prove its strictness. We examine the expressive power of commonly used branching time temporal logics. We show that CTL* has no finite base, and that almost all of its many sublogics suggested in the literature are inside the second level of our hierarchy. We introduce new Ehrenfeucht–Fraissé games on trees and use them as our main tool to prove inexpressibility.     

Logical formalisms for representing bipolar preferences

Bipolar preferences distinguish between negative preferences inducing what is acceptable by complementation and positive preferences representing what is really satisfactory. This article provides a review of the main logics for preference representation. Representing preferences in a bipolar logical way has the advantage of enabling us to reason about them, while increasing their expressive power in a cognitively meaningful way. In the article, we first focus on the possibilistic logic setting and then discuss two other logics: qualitative choice logic and penalty logic. Finally, an application of bipolar preferences querying systems is outlined. © 2008 Wiley Periodicals, Inc.     

On the extension of classical propositional logic by means of a triangular norm

In this article, we introduce a generalized extension principle by substituting a more general triangular norm T for the min intersection operator in Zadeh's extension principle. We also introduce a family of propositional logics, sup- T extension logics, obtained by the extension of classical-logical functions. A few general properties of these sup-T extension logics are derived. It is also shown that classical binary logic and the Kleene ternary logic are special cases of these logics for any choice of T, obtained by a convenient restriction of the truth domain. the very practical decomposability property of classical logic is furthermore shown to hold for the sup-min extension logic, albeit in a somewhat more limited form.     

Epistemic logic and logical omniscience II: A unifying framework

In a published paper entitled Epistemic Logic and Logical Omniscience: A Survey (Int J Intell Syst 1997, 12, 57–81) a collection of epistemic logics were reviewed and critiqued. This sequel paper provides evidence for the claim that a unifying framework for various existing epistemic logics can be defined. Of particular interest is the logic of implicit and explicit belief, the logic of awareness, and the Cadoli–Schaerf epistemic model. Although these logics appear to have surface dissimilarities, a closer examination shows that they have a strong resemblance. The contribution of this paper is to show that a unifying framework MEL (multi‐valued epistemic logic) that integrates the features of these three logics can be defined. In this paper, it is proven that the semantics of MEL subsumes the semantics of the logic of implicit and explicit belief, the logic of awareness, and the Cadoli–Schaerf epistemic model. By placing some constraints on MEL , various epistemic notions such as implicit belief, explicit belief, and awareness can be modeled. ©2000 John Wiley & Sons, Inc.     

Reasoning tractably about explicit belief: A model‐theoretic approach

Existing epistemic logics such as the logic of implicit and explicit belief and the logic of awareness adopt a deductive‐theoretic approach for characterizing belief. In this approach, an agent represents the state of the world with a conjunction of axioms in its knowledge base (KB) and evaluates queries by trying to prove or disprove that they follow from KB. This paper presents a multivalued epistemic logic (MEL) that allows agents to reason both deductively and model theoretically about implicit and explicit belief. By characterizing an agent's KB with a class of finite models, the set of formulas that an agent believes can be determined by checking their validity in all these models. This rests on the fact that MEL has a complete axiomatization (sentences that are true in all these models will also be provable). In this paper, the soundness, completeness, and decidability of MEL are proven. Furthermore, a polynomial time model‐checking algorithm for determining the satisfiability of a sentence at a particular state in a given model of MEL is also presented. © 2000 John Wiley & Sons, Inc.     

Probabilistic Logic over Paths

We introduce a probabilistic modal logic PPL extending the work of [Ronald Fagin, Joseph Y. Halpern, and Nimrod Megiddo. A logic for reasoning about probabilities. Information and Computation, 87(1,2):78–128, 1990; Ronald Fagin and Joseph Y. Halpern. Reasoning about knowledge and probability. Journal of the ACM, 41(2):340–367, 1994] by allowing arbitrary nesting of a path probabilistic operator and we prove its completeness. We prove that our logic is strictly more expressive than other logics such as the logics cited above. By considering a probabilistic extension of CTL we show that this additional expressive power is really needed in some applications.     

A decidable first-order logic for knowledge representation

Decidable first-order logics with reasonable model-theoretic semantics have several benefits for knowledge representation. These logics have the expressive power of standard first order logic along with an inference algorithm that will always terminate, both important considerations for knowledge representation. Knowledge representation systems that include a faithful implementation of one of these logics can also use its model-theoretic semantics to provide meanings for the data they store. One such logic, a variant of a simple type of first-order relevance logic, is developed and its properties described. This logic, although extremely weak, does capture a non-trivial and well-motivated set of inferences that can be entrusted to a knowledge representation system.This is a revised and much extended version of a paper of the same name that appears in the Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California, 1985.     

A complex-number Fourier technique for lower bounds on the Mod-m degree

We say an integer polynomial p, on Boolean inputs, weakly m-represents a Boolean function f if p is nonconstant and is zero (mod m), whenever f is zero. In this paper we prove that if a polynomial weakly m-represents the Mod _q function on n inputs, where q and m are relatively prime and m is otherwise arbitrary, then the degree of the polynomial is . This generalizes previous results of Barrington, Beigel and Rudich, and Tsai, which held only for constant or slowly growing m. In addition, the proof technique given here is quite different. We use a method (adapted from Barrington and Straubing) in which the inputs are represented as complex q-th roots of unity. In this representation it is possible to compute the Fourier transform using some elementary properties of the algebraic integers. As a corollary of the main theorem and the proof of Toda's theorem, if q, p are distinct primes, any depth-three circuit that computes the Mod _q function, and consists of an exact threshold gate at the output, Mod _p gates at the next level, and AND gates of polylog fan-in at the inputs, must be of exponential size. We also consider the question of how well circuits consisting of one exact gate over ACC(p)-type circuits (where p is an odd prime) can approximate parity. It is shown that such circuits must have exponential size in order to agree with parity for more than 1/2 + o(1) of the inputs. Received: February 21, 1996.     

Cut-free sequent systems for temporal logic

Currently known sequent systems for temporal logics such as linear time temporal logic and computation tree logic either rely on a cut rule, an invariant rule, or an infinitary rule. The first and second violate the subformula property and the third has infinitely many premises. We present finitary cut-free invariant-free weakening-free and contraction-free sequent systems for both logics mentioned. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics.     

Towards Behavioral Maude: Behavioral Membership Equational Logic

How can algebraic and coalgebraic specifications be integrated? How can behavioral equivalence be addressed in an algebraic specification language? The hidden-sorted approach, originating in work of Goguen and Meseguer in the early 80's, and further developed into the hidden-sorted logic approach by researchers at Oxford, UC San Diego, and Kanazawa offers some attractive answers, and has been implemented in both BOBJ and CafeOBJ. In this work we investigate both further extensions of hidden logic, and an extension of the Maude specification language called BMaude supporting this extended hidden-sorted semantics.Maude's underlying equational logic, membership equational logic, generalizes and increases the expressive power of many-sorted and order-sorted equational logics. We develop a hidden-sorted extension of membership equational logic, and give conditions under which theories have both an algebraic and a coalgebraic semantics, including final (co-)algebras. We also discuss the language design of BMaude, based on such an extended logic and using categorical notions in and across the different institutions involved. We also explain how Maude's reflective semantics provides a systematic method to extend Maude to BMaude within Maude, including module composition operations, evaluation, and automated proof methods.     

Preface: Volume 66, Issue 5

This part of the volume contains the papers accepted for presentation at the workshop on Unification in Non-Classical Logics (UNCL), co-located with ICALP 2002, which took place on July 12, 2002 in M 'alaga, Spain.The workshop was concerned with one of the most promising areas of research on non-classical logics and its applications. Unification in non-classical logics, with various approaches to handling generalised terms, has drawn more and more attention in recent years. So far, most popular lines of research include fuzzy unification of (conventional) databases and the use of fuzzy concepts in information retrieval.This workshop was conceived as a forum for the exchange of ideas relevant for the concept of unification in non-classical logics, including, but not limited to, the topics of:

• Unification in multiple-valued and fuzzy logic programming.

• Unification based on similarities and fuzzy equivalence relations.

• Categorical unification.

• Practical use of non-classical unification, e.g. in expert systems and information retrieval.

The program committee selected six papers after a reviewing process in which each submitted paper received at least two reviews. Considerable effort was devoted for the evaluation of the submissions and to providing the authors with helpful feedback. The criteria for selection were originality, quality, and relevance to the topic of the workshop.Alsinet et al reviewed and compared two models which extend first order possibilistic logic in order to enable fuzzy unification. The extension considers mainly fuzzy constants, and in form of restrictions on existential quantifiers.Banerjee and Bujosa presented a non-classical interpretion of classical unification in terms of geometrical constructions over a suitable R-module M. The main result is that unification of two terms can be seen as the intersection of their corresponding affine varieties on M. This paves the way of using methods from computer algebra in the field of unification.In Eklund et al, substitutions and unifiers appear as constructs in Kleisli categories related to particular composed powerset term monads. It is shown that an often used similarity-based approach to fuzzy unification is compatible with the categorical approach, and can be adequately extended.Kutsia presented a unification procedure for a theory with individual and sequence variables, free fixed and flexible arity function symbols and patterns. These theories have been used in different contexts such as databases, rewriting, programming languages, or theorem proving.Medina et al introduced a formal model for similarity-based fuzzy unification in multi-adjoint logic programs. On this computational model, a similarity-based unification approach which provides a semantic framework for logic programming with different notions of similarity was constructed.Virtanen introduced unification in similarity-based logic programming. One of the crucial points is the definition of similarity degrees between sets, giving rise to [lambda]-interpretations. The selection of so called most significant terms again is one of the cornerstones of the paper.We would like to thank all those who submitted papers for consideration, the authors of accepted papers for their interesting discussions during the workshop, the additional referees for their careful work, and Inma Fortes from the local organising committee for her assistance.     

A novel multiple-attribute group decision-making method based on q-rung orthopair fuzzy generalized power weighted aggregation operators

In this paper, a novel approach is developed to deal with multiple-attribute group decision-making (MAGDM) problem under q-rung orthopair fuzzy environment. Firstly, some operators have been proposed to aggregate q-rung orthopair fuzzy information, such as the q-rung orthopair fuzzy generalized power averaging (q-ROFGPA) operator, the q-rung orthopair fuzzy generalized power weighted averaging (q-ROFGPWA) operator, the q-rung orthopair fuzzy generalized power geometric (q-ROFGPG) operator, and the q-rung orthopair fuzzy generalized power weighted geometric (q-ROFGPWG) operator. In addition, some desirable properties and special cases of these operators are discussed. Second, a novel approach is developed to solve MAGDM problem under the q-rung orthopair fuzzy environment based on the proposed q-ROFGPWA and q-ROFGPWG operators. Finally, a practical example is given to illustrate the application of the proposed method, and further the sensitivity analysis and comparative analysis are carried out.     

A Review of Literature: Individual Blame vs. Organizational Function Logics in Accident Analysis

When an accident happens in an organization, two different approaches are possible to explain its origin and dynamics. The first approach, called individual blame logic aims at finding the guilty individuals. The second approach, called organizational function logic aims to identify the organizational factors that favoured the occurrence of the event. This article compares the two different logics of inquiry, the consequences that they produce, in particular in the case of accidents caused by unintentional actions. Though favoured by the scientists, the organizational function logic approach is in real life usually beaten by the individual blame logic. Reviewing the literature, this article brings together the arguments for using the organizational function logic from the perspective that learning from accidents is necessary to prevent them from happening again.     

Studying properties of classes of default logics

The study of different variants of default logic reveals not only differences but also properties they share. For example, there seems to be a close relationship between semi-monotonicity and the guaranteed existence of extensions. Likewise, formula-manipulating default logics tend to violate the property of cumulativity. The problem is that currently such properties must be established separately for each approach. This paper describes some steps towards the study of properties of classes of default logics by giving a rather general definition of what a default logic is. Essentially our approach is operational and restricts attention to purely formula-manipulating logics. We motivate our definition and demonstrate that it includes a variety of well-known default logics. Furthermore, we derive general results regarding the concepts of semi-monotonicity and cumulativity. As a benefit of the discussion we uncover that some design decisions of concrete default logics were not accidental as they may seem, but rather they were due to objective necessities.     

A Restricted Second Order Logic for Finite Structures

We introduce a restricted version of second order logic SO^ωin which the second order quantifiers range over relations that are closed under the equivalence relation ≡^kofkvariable equivalence, for somek. This restricted second order logic is an effective fragment of the infinitary logicL^ω_∞ω, but it differs from other such fragments in that it is not based on a fixed point logic. We explore the relationship of SO^ωwith fixed point logics, showing that its inclusion relations with these logics are equivalent to problems in complexity theory. We also look at the expressibility of NP-complete problems in this logic.