Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userProcessor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic
99
0
0.0
(
0
)
Added by
Randal E. Bryant
Publication date
1999
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
The logic of equality with uninterpreted functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas, we can apply Boolean methods such as Ordered Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification. We can exploit characteristics of the formulas describing the verification conditions to greatly simplify the propositional formulas generated. In particular, we exploit the property that many equations appear only in positive form. We can therefore reduce the set of interpretations of the function symbols that must be considered to prove that a formula is universally valid to those that are ``maximally diverse. We present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill.
rate research
Read More
We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagners counting hierarchy, but also that the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is derived in the spirit of the Curry-Howard correspondence, showing the potential of counting propositional logic as a useful tool in several fields of theoretical computer science.
The model checking problem for propositional dynamic logic (PDL) over message sequence charts (MSCs) and communicating finite state machines (CFMs) asks, given a channel bound $B$, a PDL formula $varphi$ and a CFM $mathcal{C}$, whether every existentially $B$-bounded MSC $M$ accepted by $mathcal{C}$ satisfies $varphi$. Recently, it was shown that this problem is PSPACE-complete. In the present work, we consider CRPDL over MSCs which is PDL equipped with the operators converse and repeat. The former enables one to walk back and forth within an MSC using a single path expression whereas the latter allows to express that a path expression can be repeated infinitely often. To solve the model checking problem for this logic, we define message sequence chart automata (MSCAs) which are multi-way alternating parity automata walking on MSCs. By exploiting a new concept called concatenation states, we are able to inductively construct, for every CRPDL formula $varphi$, an MSCA precisely accepting the set of models of $varphi$. As a result, we obtain that the model checking problem for CRPDL and CFMs is still in PSPACE.
Description Logics (DLs) are a family of languages used for the representation and reasoning on the knowledge of an application domain, in a structured and formal manner. In order to achieve this objective, several provers, such as RACER and FaCT++, have been implemented, but these provers themselves have not been yet certified. In order to ensure the soundness of derivations in these DLs, it is necessary to formally verify the deductions applied by these reasoners. Formal methods offer powerful tools for the specification and verification of proof procedures, among them there are methods for proving properties such as soundness, completeness and termination of a proof procedure. In this paper, we present the definition of a proof procedure for the Description Logic ALC, based on a semantic tableau method. We ensure validity of our prover by proving its soundness, completeness and termination properties using Isabelle proof assistant. The proof proceeds in two phases, first by establishing these properties on an abstract level, and then by instantiating them for an implementation based on lists.
Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. Short-circuit evaluation is widely used in programming, with sequential conjunction and disjunction as primitive connectives. We study the question which logical laws axiomatize short-circuit evaluation under the following assumptions: compound statements are evaluated from left to right, each atom (propositional variable) evaluates to either true or false, and atomic evaluations can cause a side effect. The answer to this question depends on the kind of atomic side effects that can occur and leads to different short-circuit logics. The basic case is FSCL (free short-circuit logic), which characterizes the setting in which each atomic evaluation can cause a side effect. We recall some main results and then relate FSCL to MSCL (memorizing short-circuit logic), where in the evaluation of a compound statement, the first evaluation result of each atom is memorized. MSCL can be seen as a sequential variant of propositional logic: atomic evaluations cannot cause a side effect and the sequential connectives are not commutative. Then we relate MSCL to SSCL (static short-circuit logic), the variant of propositional logic that prescribes short-circuit evaluation with commutative sequential connectives. We present evaluation trees as an intuitive semantics for short-circuit evaluation, and simple equational axiomatizations for the short-circuit logics mentioned that use negation and the sequential connectives only.
In the present paper we consider the simplest non-classical extension $GL4$ of the well-known propositional provability logic $GL$ together with the notion of expressibility of formulas in a logic proposed by A. V. Kuznetsov. Conditions for expressibility of constants in the 4-valued extension $Lmathfrak{B}_2$ of $GL$ are found out, which were first announced in a authors paper in 1996.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
