Formal modeling and verification (in PVS) of multi-agent system architecture

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en PVS sobre multi agentes titulado Formal modeling and verification of multi-agent system architecture.

Sus autores son

  • Ling Yuan (de la Huazhong University of Science and Technology, Wuhan, China) y
  • Ping Fan (de la Hubei University of Science and Technology, Hubei, China).

Su resumen es

In a multi-agent system, the multiple distributed intelligent agents interact with each other to solve problems. To guide the development of multi-agent system, the multi-agent system architecture would provide a framework. The specific multi- agent system can be customized from the multi-agent system architecture, which does not need to rewrite the construction. In order to satisfy the failure recovery property of multi-agent system, we propose dependable multi-agent system architecture with fault tolerant mechanisms. The PVS formal language is used to build a system architecture, which can provide common patterns and idioms to the system developers. In order to satisfy the reliability requirements, the powerful PVS theorem prover can be used to analyze the high reliability property of the proposed architecture.

El trabajo se ha presentado en la 2013 AASRI Conference on Parallel and Distributed Computing and Systems.

Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre
teoría de grafos titulado Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem.

Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).

Su resumen es

The Girth-Chromatic number theorem is a theorem from graph theory, stating that graphs with arbitrarily large girth and chro- matic number exist. We formalize a probabilistic proof of this theorem in the Isabelle/HOL theorem prover, closely following a standard textbook proof and use this to explore the use of the probabilistic method in a theorem prover.

El trabajo se presentó en el ITP 2012 (Interactive Theorem Proving).

El código de las correspondientes teorías en Isabelle se encuentra aquí.

Reseña: A graph library for Isabelle

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle titulado A graph library for Isabelle.

Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).

Su resumen es

In contrast to other areas of such as analysis, number theory or probability theory, no standard library for graph theory has yet evolved for the Isabelle/HOL proof assistant. We present a formalization of directed graphs and essential related concepts. The library supports general infinite directed graphs (digraphs) with labeled and parallel arcs, but care has been taken not to complicate reasoning on more restricted classes of digraphs.

We use this library to formalize a characterization of Euler Digraphs and a to verify a method of checking Kuratowski subgraphs used in the LEDA library.

El código de la teoría en Isabelle se encuentra aquí.

Gödel’s incompleteness theorems

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento aproximado en Isabelle/HOL sobre metalógica titulado Gödel’s incompleteness theorems.

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

Gödel’s two incompleteness theorems are formalised, following a careful presentation by Swierczkowski, in the theory of hereditarily finite sets. This represents the first ever machine-assisted proof of the second incompleteness theorem. Compared with traditional formalisations using Peano arithmetic (see e.g. Boolos), coding is simpler, with no need to formalise the notion of multiplication (let alone that of a prime number) in the formalised calculus upon which the theorem is based. However, other technical problems had to be solved in order to complete the argument.

El trabajo se ha publicado en The Archive of Formal Proofs

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

The hereditarily finite sets

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento aproximado en Isabelle/HOL sobre la teoría de conjuntos titulado The hereditarily finite sets.

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

The theory of hereditarily finite (HF) sets is formalised, following the development of Swierczkowski. An HF set is a finite collection of other HF sets; they enjoy an induction principle and satisfy all the axioms of ZF set theory apart from the axiom of infinity, which is negated. All constructions that are possible in ZF set theory (Cartesian products, disjoint sums, natural numbers, functions) without using infinite sets are possible here. The definition of addition for the HF sets follows Kirby.

This development forms the foundation for the Isabelle proof of Gödel’s incompleteness theorems, which has been formalised separately.

El trabajo se ha publicado en The Archive of Formal Proofs.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.