3 citations · 4 across the 5 of their papers we have counts for
5 papers
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
Cheng Zhang, Qiancheng Fu, Hang Ji +3
This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate a…
Kleene algebra with commutativity conditions is undecidable
Arthur Azevedo de Amorim, Cheng Zhang, Marco Gaboardi
We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in…
CF-GKAT: Efficient Validation of Control-Flow Transformations
Cheng Zhang, Tobias Kappé, David E. Narváez +1
Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still seve…
Domain Reasoning in TopKAT
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the to…
Finite-memory Strategies for Almost-sure Energy-MeanPayoff Objectives in MDPs
Mohan Dantam, Richard Mayr
We consider finite-state Markov decision processes with the combined Energy-MeanPayoff objective. The controller tries to avoid running out of energy while simultaneously attaining…