O dynamické logice
Object oriented institutions to specify symbolic computation systems
The specification of the data structures used in EAT, a software system for symbolic computation in algebraic topology, is based on an operation that defines a link among different specification frameworks like hidden algebras and coalgebras. In this paper, this operation is extended using the notion of institution, giving rise to three institution encodings. These morphisms define a commutative diagram which shows three possible views of the same construction, placing it in an equational algebraic...
On characteristic formulae for Event-Recording Automata
A standard bridge between automata theory and logic is provided by the notion of characteristic formula. This paper investigates this problem for the class of event-recording automata (ERA), a subclass of timed automata in which clocks are associated with actions and that enjoys very good closure properties. We first study the problem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), a logic introduced by Sorea to express event-based timed specifications. We prove that...
On distributive fixed-point expressions
On Distributive Fixed-Point Expressions
For every fixed-point expression e of alternation-depth r, we construct a new fixed-point expression e' of alternation-depth 2 and size . Expression e' is equivalent to e whenever operators are distributive and the underlying complete lattice has a co-continuous least upper bound. We alternation-depth but also w.r.t. the increase in size of the resulting expression.
On global induction mechanisms in a -calculus with explicit approximations
We investigate a Gentzen-style proof system for the first-order -calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...
On global induction mechanisms in a μ-calculus with explicit approximations
We investigate a Gentzen-style proof system for the first-order μ-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...
On Lamport's comparison between linear and branching time temporal logic
On proofs of correctness of well-structured programs
On proofs of correctness of well-structured programs. II
On some arithmetically expressible properties of programs
On temporal program verification rules
On the Decidability of the Equivalence Problem for Monadic Recursive Programs
We present a uniform and easy-to-use technique for deciding the equivalence problem for deterministic monadic linear recursive programs. The key idea is to reduce this problem to the well-known group-theoretic problems by revealing an algebraic nature of program computations. We show that the equivalence problem for monadic linear recursive programs over finite and fixed alphabets of basic functions and logical conditions is decidable in polynomial time for the semantics based on the free monoids...
On the use of homomorphisms for proving the equivalence of some programs