Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn Refinements of Boolean and Parametric Modal Transition Systems
109
0
0.0
(
0
)
Added by
Jan K\\v{r}et\\'insk\\'y
Publication date
2013
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We consider the extensions of modal transition systems (MTS), namely Boolean MTS and parametric MTS and we investigate the refinement problems over both classes. Firstly, we reduce the problem of modal refinement over both classes to a problem solvable by a QBF solver and provide experimental results showing our technique scales well. Secondly, we extend the algorithm for thorough refinement of MTS providing better complexity then via reductions to previously studied problems. Finally, we investigate the relationship between modal and thorough refinement on the two classes and show how the thorough refinement can be approximated by the modal refinement.
rate research
Read More
We introduce a logical framework for the specification and verification of component-based systems, in which finitely many component instances are active, but the bound on their number is not known. Besides specifying and verifying parametric systems, we consider the aspect of dynamic reconfiguration, in which components can migrate at runtime on a physical map, whose shape and size may change. We describe such parametric and reconfigurable architectures using resource logics, close in spirit to Separation Logic, used to reason about dynamic pointer structures. These logics support the principle of local reasoning, which is the key for writing modular specifications and building scalable verification algorithms, that deal with large industrial-size systems.
Modern CDCL SAT solvers easily solve industrial instances containing tens of millions of variables and clauses, despite the theoretical intractability of the SAT problem. This gap between practice and theory is a central problem in solver research. It is believed that SAT solvers exploit structure inherent in industrial instances, and hence there have been numerous attempts over the last 25 years at characterizing this structure via parameters. These can be classified as rigorous, i.e., they serve as a basis for complexity-theoretic upper bounds (e.g., backdoors), or correlative, i.e., they correlate well with solver run time and are observed in industrial instances (e.g., community structure). Unfortunately, no parameter proposed to date has been shown to be both strongly correlative and rigorous over a large fraction of industrial instances. Given the sheer difficulty of the problem, we aim for an intermediate goal of proposing a set of parameters that is strongly correlative and has good theoretical properties. Specifically, we propose parameters based on a graph partitioning called Hierarchical Community Structure (HCS), which captures the recursive community structure of a graph of a Boolean formula. We show that HCS parameters are strongly correlative with solver run time using an Empirical Hardness Model, and further build a classifier based on HCS parameters that distinguishes between easy industrial and hard random/crafted instances with very high accuracy. We further strengthen our hypotheses via scaling studies. On the theoretical side, we show that counterexamples which plagued community structure do not apply to HCS, and that there is a subset of HCS parameters such that restricting them limits the size of embeddable expanders.
In this paper an algorithm is designed which generates in-equivalent Boolean functions of any number of variables from the four Boolean functions of single variable. The grammar for such set of Boolean function is provided. The Turing Machine that accepts such set is constructed.
A well-known problem in Petri net theory is to formalise an appropriate causality-based concept of process or run for place/transition systems. The so-called individual token interpretation, where tokens are distinguished according to their causal history, giving rise to the processes of Goltz and Reisig, is often considered too detailed. The problem of defining a fully satisfying more abstract concept of process for general place/transition systems has so-far not been solved. In this paper, we recall the proposal of defining an abstract notion of process, here called BD-process, in terms of equivalence classes of Goltz-Reisig processes, using an equivalence proposed by Best and Devillers. It yields a fully satisfying solution for at least all one-safe nets. However, for certain nets which intuitively have different conflicting behaviours, it yields only one maximal abstract process. Here we identify a class of place/transition systems, called structural conflict nets, where conflict and concurrency due to token multiplicity are clearly separated. We show that, in the case of structural conflict nets, the equivalence proposed by Best and Devillers yields a unique maximal abstract process only for conflict-free nets. Thereby BD-processes constitute a simple and fully satisfying solution in the class of structural conflict nets.
We introduce frame-equivalence games tailored for reasoning about the size, modal depth, number of occurrences of symbols and number of different propositional variables of modal formulae defining a given frame-property. Using these games, we prove lower bounds on the above measures for a number of well-known modal axioms; what is more, for some of the axioms, we show that they are optimal among the formulae defining the respective class of frames.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
