enter search term and/or author name
Traditional automata accept or reject their input and are therefore Boolean. In contrast, weighted automata map each word to a value from a semiring over a large domain. The special case of lattice automata, in which the semiring is a...
Logical Characterizations of Behavioral Relations on Transition Systems of Probability Distributions
Silvia Crafa, Francesco Ranzato
Article No.: 2
Probabilistic nondeterministic processes are commonly modeled as probabilistic LTSs (PLTSs). A number of logical characterizations of the main behavioral relations on PLTSs have been studied. In particular, Parma and Segala  and Hermanns et...
A Conceptual Framework for Secrecy-preserving Reasoning in Knowledge Bases
Jia Tao, Giora Slutzki, Vasant Honavar
Article No.: 3
In many applications, Knowledge Bases (KBs) contain confidential or private information (secrets). The KB should be able to use this secret information in its reasoning process but in answering user queries care must be exercised so that secrets...
Decidability of Approximate Skolem Problem and Applications to Logical Verification of Dynamical Properties of Markov Chains
M. Biscaia, D. Henriques, P. Mateus
Article No.: 4
When studying probabilistic dynamical systems, temporal logic has typically been used to analyze path properties. Recently, there has been some interest in analyzing the dynamical evolution of state probabilities of these systems. In this article,...
Taming Paraconsistent (and Other) Logics: An Algorithmic Approach
Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky
Article No.: 5
We develop a fully algorithmic approach to “taming” logics expressed Hilbert style, that is, reformulating them in terms of analytic sequent calculi and useful semantics. Our approach applies to Hilbert calculi extending the positive...
Partially specified systems and specifications are used in formal methods such as stepwise design and query checking. Existing methods consider a setting in which systems and their correctness are Boolean. In recent years, there has been growing...
Why Is It Hard to Obtain a Dichotomy for Consistent Query Answering?
Article No.: 7
A database may for various reasons become inconsistent with respect to a given set of integrity constraints. In the late 1990s, the formal approach of consistent query answering was proposed in order to query such databases. Since then, a lot of...
It is well known that G3i, the sequent calculus for intuitionistic propositional logic where weakening and contraction are absorbed into the rules, is not terminating. Indeed, due to the contraction in the rule for left implication, the naïve...
The Complexity of Decomposing Modal and First-Order Theories
Stefan Göller, Jean-Christoph Jung, Markus Lohrey
Article No.: 9
We study the satisfiability problem of the logic K2 &equal; K × K—the two-dimensional variant of unimodal logic, where models are restricted to asynchronous products of two Kripke frames. Gabbay and Shehtman proved in 1998...