О системах переписывания процессов высокого уровня

Системы переписывания процессов (Process Rewrite Systems - PRS) Ричарда Майра представляют собой систему переписывания термов специального вида и задают унифицированное представление для конечных и магазинных автоматов, сетей Петри и некоторых классов алгебр процессов. В докладе рассматривается (P,P)-подкласс систем переписывания процессов, соответствующий классическим сетям Петри, и его расширение HPRS для моделирования систем с динамической структурой. Обсуждаются вопросы выразительности и разрешимости.

CoCo 2019: report on the eighth confluence competition

We report on the 2019 edition of the Confluence Competition, a competition of software tools that aim to prove or disprove confluence and related (undecidable) properties of rewrite systems automatically.

Certifying Proofs in the First-Order Theory of Rewriting

The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present , a reincarnation of the decision tool with certifiable output, and the formally verified certifier .

Computing knowledge in equational extensions of subterm convergent theories

We study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system (TRS). In this work, we extend this to consider a subterm convergent TRS defined modulo an equational theory, like Commutativity. We present two pairs of solutions for these important problems. The first solves the deduction and static equivalence problems in rewrite systems modulo shallow theories such as Commutativity. The second provides a general procedure that solves the deduction and static equivalence problems in subterm convergent systems modulo syntactic permutative theories, provided a finite measure is ensured. Several examples of such theories are also given.

A proof-theoretic study of abstract termination principles

We carry out a proof-theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees that can be defined in Gödel’s system T plus bar recursion. We then carry out a complexity analysis of these terms and demonstrate how this can be applied to bound the derivational height of term rewrite systems.