Abstract: Jan Friso Groote, David N. Jansen, Jeroen J. A. Keiren, Anton J. Wijs
We provide a new algorithm to determine stuttering equivalence with time complexity O(mlogn), where n is the number of states and m is the number of transitions of a Kripke structure. This algorithm can also be used to determine branching bisimulation in O(m(log |Act| + log n)) time, where Act is the set of actions in a labeled transition system. Theoretically, our algorithm substantially improves upon existing algorithms, which all have time complexity of the form O(mn) at best. Moreover, it has better or equal space complexity. Practical results confirm these findings: they show that our algorithm can outperform existing algorithms by several orders of magnitude, especially when the Kripke structures are large. PubDate: Fri, 23 Jun 2017 00:00:00 GMT
In many tasks related to reasoning about consequences of a logical theory, it is desirable to decompose the theory into a number of weakly related or independent components. However, a theory may represent knowledge that is subject to change, as a result of executing actions that have effects on some of the initial properties mentioned in the theory. Having once computed a decomposition of a theory, it is advantageous to know whether a decomposition has to be computed again in the newly changed theory (obtained from taking into account changes resulting from execution of an action). In this article, we address this problem in the scope of the situation calculus, where a change of an initial theory is related to the notion of progression. PubDate: Fri, 23 Jun 2017 00:00:00 GMT
We study consistency search problems for Frege and extended Frege proofs—namely the NP search problems of finding syntactic errors in Frege and extended Frege proofs of contradictions. The input is a polynomial time function, or an oracle, describing a proof of a contradiction; the output is the location of a syntactic error in the proof. The consistency search problems for Frege and extended Frege systems are shown to be many-one complete for the provably total NP search problems of the second-order bounded arithmetic theories U12 and V12, respectively. PubDate: Fri, 02 Jun 2017 00:00:00 GMT
This article aims to develop a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we extend transformation methods based on integer term rewriting systems to handle arbitrary data types, global variables, function calls, and arrays, and to encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. PubDate: Fri, 02 Jun 2017 00:00:00 GMT
Abstract: Che-Ping Su, Tuan-Fang Fan, Churn-Jung Liau
Justification logic originated from the study of the logic of proofs. However, in a more general setting, it may be regarded as a kind of explicit epistemic logic. In such logic, the reasons a fact is believed are explicitly represented as justification terms. Traditionally, the modeling of uncertain beliefs is crucially important for epistemic reasoning. Graded modal logics interpreted with possibility theory semantics have been successfully applied to the representation and reasoning of uncertain beliefs; however, they cannot keep track of the reasons an agent believes a fact. This article is aimed at extending the graded modal logics with explicit justifications. PubDate: Fri, 02 Jun 2017 00:00:00 GMT
Abstract: Nicholas R. Radcliffe, Luis F. T. Moraes, Rakesh M. Verma
Uniqueness of normal forms (UN=) is an important property of term rewrite systems. UN= is decidable for ground (i.e., variable-free) systems and undecidable in general. Recently, it was shown to be decidable for linear, shallow systems. We generalize this previous result and show that this property is decidable for shallow rewrite systems, in contrast to confluence, reachability, and other related properties, which are all undecidable for flat systems. We also prove an upper bound on the complexity of our algorithm. PubDate: Fri, 02 Jun 2017 00:00:00 GMT
Abstract: Przemysław Daca, Thomas A. Henzinger, Jan Křetínský, Tatjana Petrov
We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. PubDate: Mon, 29 May 2017 00:00:00 GMT
Abstract: Szymon Chlebowski, Maciej Komosinski, Adam Kups
This article concerns automated generation and processing of erotetic search scenarios (ESSs). ESSs are formal constructs characterized in Inferential Erotetic Logic that enable finding possible answers to a posed question by decomposing it into auxiliary questions. The first part of this work describes a formal account on ESSs. The formal approach is then applied to automatically generate ESSs, and the resulting scenarios are evaluated according to a number of criteria. These criteria are subjected to discordance analysis that reveals their mutual relationships. Finally, knowledge concerning relationships between different values of evaluation criteria is extracted by applying Apriori—an association rules mining algorithm. PubDate: Fri, 05 May 2017 00:00:00 GMT
Stable model semantics had been recently generalized to non-Herbrand structures by several works, which provides a unified framework and solid logical foundations for answer set programming. This article focuses on the expressiveness of normal and disjunctive logic programs under general stable model semantics. A translation from disjunctive logic programs to normal logic programs is proposed for infinite structures. Over finite structures, some disjunctive logic programs are proved to be intranslatable to normal logic programs if the arities of auxiliary predicates and functions are bounded in a certain way. The equivalence of the expressiveness of normal logic programs and disjunctive logic programs over arbitrary structures is also shown to coincide with that over finite structures and coincide with whether the complexity class NP is closed under complement. PubDate: Fri, 05 May 2017 00:00:00 GMT
Graph databases make use of logics that combine traditional first-order features with navigation on paths, in the same way logics for model checking do. However, modern applications of graph databases impose a new requirement on the expressiveness of the logics: they need comparing labels of paths based on word relations (such as prefix, subword, or subsequence). This has led to the study of logics that extend basic graph languages with features for comparing labels of paths based on regular relations or the strictly more powerful rational relations. The evaluation problem for the former logic is decidable (and even tractable in data complexity), but already extending this logic with such a common rational relation as subword or suffix makes evaluation undecidable. PubDate: Fri, 05 May 2017 00:00:00 GMT
Hybrid journal (It can contain Open Access articles)
[45 journals]
