DKAL and Z3: A logic embedding experiment

Yuri Gurevich and Itay Neeman proposed the Distributed Knowledge Authorization Language, DKAL, as an expressive, yet very succinct logic for distributed authorization. DKAL uses a combination of modal and intuitionistic propositional logic. Modalities are used for qualifying assertions made by diffe...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Mera, S., Bjørner, N.
Formato: SER
Materias:
DKAL
Embedding
Model Extraction
Z3
Authorization languages
Distributed authorization
Distributed knowledge
First-order
Intuitionistic logic
Non-trivial
Propositional logic
Root cause
Satisfiability modulo Theories
Computer science
Technical presentations
Formal logic
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v6300LNCS_n_p504_Mera
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_03029743_v6300LNCS_n_p504_Mera
record_format dspace
spelling todo:paper_03029743_v6300LNCS_n_p504_Mera2023-10-03T15:19:15Z DKAL and Z3: A logic embedding experiment Mera, S. Bjørner, N. DKAL Embedding Model Extraction Z3 Authorization languages Distributed authorization Distributed knowledge DKAL Embedding First-order Intuitionistic logic Model Extraction Non-trivial Propositional logic Root cause Satisfiability modulo Theories Z3 Computer science Technical presentations Formal logic Yuri Gurevich and Itay Neeman proposed the Distributed Knowledge Authorization Language, DKAL, as an expressive, yet very succinct logic for distributed authorization. DKAL uses a combination of modal and intuitionistic propositional logic. Modalities are used for qualifying assertions made by different principals and intuitionistic logic captures very elegantly assertions about basic information. Furthermore, a non-trivial and useful fragment known as the primal infon logic is amenable to efficient linear-time saturation. In this paper we experiment with an embedding of the full DKAL logic into the state-of-the-art Satisfiability Modulo Theories solver Z3 co-developed by the second author. Z3 supports classical first-order semantics of formulas, so it is not possible to directly embed DKAL into Z3. We therefore use an indirect encoding. The one experimented with in this paper uses the instantiation-based support for quantifiers in Z3. Z3 offers the feature to return a potential ground counter-model when the saturation procedure ends up with a satisfiable set of ground assertions. We develop an algorithm that extracts a DKAL model from the propositional model, in order to provide root causes for non-derivability. © 2010 Springer-Verlag Berlin Heidelberg. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v6300LNCS_n_p504_Mera
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic DKAL
Embedding
Model Extraction
Z3
Authorization languages
Distributed authorization
Distributed knowledge
DKAL
Embedding
First-order
Intuitionistic logic
Model Extraction
Non-trivial
Propositional logic
Root cause
Satisfiability modulo Theories
Z3
Computer science
Technical presentations
Formal logic
spellingShingle DKAL
Embedding
Model Extraction
Z3
Authorization languages
Distributed authorization
Distributed knowledge
DKAL
Embedding
First-order
Intuitionistic logic
Model Extraction
Non-trivial
Propositional logic
Root cause
Satisfiability modulo Theories
Z3
Computer science
Technical presentations
Formal logic
Mera, S.
Bjørner, N.
DKAL and Z3: A logic embedding experiment
topic_facet DKAL
Embedding
Model Extraction
Z3
Authorization languages
Distributed authorization
Distributed knowledge
DKAL
Embedding
First-order
Intuitionistic logic
Model Extraction
Non-trivial
Propositional logic
Root cause
Satisfiability modulo Theories
Z3
Computer science
Technical presentations
Formal logic
description Yuri Gurevich and Itay Neeman proposed the Distributed Knowledge Authorization Language, DKAL, as an expressive, yet very succinct logic for distributed authorization. DKAL uses a combination of modal and intuitionistic propositional logic. Modalities are used for qualifying assertions made by different principals and intuitionistic logic captures very elegantly assertions about basic information. Furthermore, a non-trivial and useful fragment known as the primal infon logic is amenable to efficient linear-time saturation. In this paper we experiment with an embedding of the full DKAL logic into the state-of-the-art Satisfiability Modulo Theories solver Z3 co-developed by the second author. Z3 supports classical first-order semantics of formulas, so it is not possible to directly embed DKAL into Z3. We therefore use an indirect encoding. The one experimented with in this paper uses the instantiation-based support for quantifiers in Z3. Z3 offers the feature to return a potential ground counter-model when the saturation procedure ends up with a satisfiable set of ground assertions. We develop an algorithm that extracts a DKAL model from the propositional model, in order to provide root causes for non-derivability. © 2010 Springer-Verlag Berlin Heidelberg.
format SER
author Mera, S.
Bjørner, N.
author_facet Mera, S.
Bjørner, N.
author_sort Mera, S.
title DKAL and Z3: A logic embedding experiment
title_short DKAL and Z3: A logic embedding experiment
title_full DKAL and Z3: A logic embedding experiment
title_fullStr DKAL and Z3: A logic embedding experiment
title_full_unstemmed DKAL and Z3: A logic embedding experiment
title_sort dkal and z3: a logic embedding experiment
url http://hdl.handle.net/20.500.12110/paper_03029743_v6300LNCS_n_p504_Mera
work_keys_str_mv AT meras dkalandz3alogicembeddingexperiment
AT bjørnern dkalandz3alogicembeddingexperiment
_version_ 1782028765075865600

Ejemplares similares