max planck institut
informatik
informatik
Abstract:
The distributed synthesis problem is to transform a logical
specification into a collection of processes that, when composed
according to a given system architecture, satisfy the specification.
In this talk I will describe two approaches for distributed synthesis
from linear-time temporal logic. The first solution, based on
automata-theoretic transformations, provides a general decision
procedure for all architectures with decidable synthesis problems,
but has non-elementary complexity. The second solution reduces
the synthesis problem to an SMT problem, where the
existence of a distributed implementation is specified as a quantified
formula in the theory (N,<) of the ordered natural numbers with
uninterpreted function symbols. While our experimental results
indicate that the resulting satisfiability problem is generally out of
reach for the currently available SMT solvers, the problem becomes
tractable if we fix an upper bound on the number of states in the
distributed system. By iteratively increasing the bound, we obtain an
effective semi-decision procedure for distributed synthesis.
The talk is based on joint work with Sven Schewe.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Abstract:
Hybrid logic and modal logic with the difference
modality (MLD) are modal logics with equality.
Despite recent advances for hybrid logic, terminating
tableau systems for MLD have remained a challenge.
The established decision procedure [Balbiani and
Demri 1997] does not terminate for all inputs, and a
terminating tableau system for MLD with inverse
modalities was not known.
I will report about ongoing work with Mark Kaminski
and present a terminating tableau system for
a modal logic MLE that subsumes hybrid logic and MLD.
Our approach avoids the syntactic limitations of
modal logic by representing MLE as a fragment of
simple type theory. This way the connection between
MLE and pure predicate logic with equality (PLE)
becomes formal. PLE subsumes MLE up to translation,
and the terminating tableau system for MLE appears as
a refinement of a complete tableau system for PLE.
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).
Abstract:
We present a general framework which allows to identify complex theories
important in verification for which efficient reasoning methods exist.
The framework we present is based on a general notion of locality.
We show that locality considerations allow us to obtain parameterized
decidability and complexity results for many (combinations of) theories
important in verification in general and in the verification of parametric
systems in particular.
We give numerous examples; in particular we show that several theories
of data structures studied in the verification literature -- e.g.
various theories of pointer structures and of arrays -- can be seen as
local extensions of a base theory.
The general framework we use allows us to identify situations in which
some of the syntactical restrictions imposed in previous papers can be
relaxed.
(The talk is based on joint work with Carsten Ihlemann and Swen Jacobs.)
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).
Abstract:
Knowledge Compilation is a common technique for propositional logic
knowledge bases. The idea is to transform a given knowledge base into a
special normal form, for which queries can be answered efficiently. We
propose to apply this technique to knowledge bases defined in
Description Logic.
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).
Abstract:
We introduce a new rule-based formalism - OWL1.1 Rules - for knowledge
representation and reasoning for the Semantic Web. OWL1.1 Rules have the
following features:
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here (+ Video). Copyright with the author(s).
Abstract:
We present a new algorithm for reasoning in the description logic SHIQ, which
is the most prominent fragment of the Web Ontology Language OWL. The algorithm
is based on ordered binary decision diagrams (OBDDs) as a datastructure for
storing and operating on large model representations. We thus draw on the
success and the proven scalability of OBDD-based systems. To the best of
our knowledge, we present the very first algorithm for using OBDDs for
reasoning with general TBoxes.
The slides to the presentation can be found here. Copyright with the author(s).
The slides to the presentation can be found here. Copyright with the author(s).