opinionated
发表于 2025-3-23 13:19:32
Concurrent Kleene Algebra with Testsconcurrency inequation and have a Kleene-star for both sequential and concurrent composition. Kleene algebra with tests (KAT) were defined earlier by Kozen and Smith . . (CKAT) combine these concepts and give a relatively simple algebraic model for reasoning about operational semantics of conc
characteristic
发表于 2025-3-23 17:39:40
Algebras for Program Correctness in Isabelle/HOLations of tests. Our structured comprehensive libraries for these algebras extend an existing Kleene algebra library. It includes an algebraic account of Hoare logic for partial correctness and several refinement and concurrency control laws in a total correctness setting. Formalisation examples inc
CLAIM
发表于 2025-3-23 19:51:32
http://reply.papertrans.cn/83/8262/826122/826122_13.png
FLING
发表于 2025-3-24 00:38:38
A Modified Completeness Theorem of KAT and Decidability of Term Reducibility formulas ∧ ... = .. → . = . in KAT has been studied so far by several researchers. Continuing this line of research, this paper studies the decidability of existentially quantified equational formulas ∃ . ∈ P. (. = .) in KAT, where P is a fixed collection of KAT terms. A new completeness theorem of
harangue
发表于 2025-3-24 05:40:16
Kleene Algebra with Converseas studied by Bernátsky, Bloom, Ésik, and Stefanescu in 1995. We reformulate some of their proofs in syntactic and elementary terms, and we provide a new algorithm to decide the corresponding theory. This algorithm is both simpler and more efficient; it relies on an alternative automata construction
Magnitude
发表于 2025-3-24 09:18:10
http://reply.papertrans.cn/83/8262/826122/826122_16.png
Lucubrate
发表于 2025-3-24 11:10:55
Extended Conscriptions Algebraicallyt to initial states. We show that they instantiate existing algebras for iteration and infinite computations. We use these algebras to derive an approximation order for conscriptions and one for extended conscriptions, which additionally represent aborting executions. We give a new computation model
隐语
发表于 2025-3-24 18:18:10
Abstract Dynamic Frames concepts, properties and behaviour of that theory in a pointfree fashion. Moreover, relationships to abstract concepts of separation logic are given to pave the way for a unified treatment of both approaches. In particular, we also sketch the main ideas within the framework of local actions.
Affiliation
发表于 2025-3-24 22:18:47
http://reply.papertrans.cn/83/8262/826122/826122_19.png
Inscrutable
发表于 2025-3-25 01:22:34
On Faults and Faulty Programstails unspecified. An incorrect program may be corrected in many different ways, involving different numbers of modifications. Hence neither the location nor the number of of faults may be defined in a unique manner; this, in turn, sheds a cloud of uncertainty on such concepts as fault density, and