scholarly journals A Deductive Approach towards Reasoning about Algebraic Transition Systems

2015 ◽  
Vol 2015 ◽  
pp. 1-12
Author(s):  
Jun Fu ◽  
Jinzhao Wu ◽  
Hongyan Tan
Keyword(s):  
Complex Systems ◽  
Dynamic Logic ◽  
Decision Procedures ◽  
Proof System ◽  
Search Problem ◽  
Inference Rules ◽  
Algebraic Equations ◽  
Transition Systems ◽  
Proof Search ◽  
Polynomial Ideals

Algebraic transition systems are extended from labeled transition systems by allowing transitions labeled by algebraic equations for modeling more complex systems in detail. We present a deductive approach for specifying and verifying algebraic transition systems. We modify the standard dynamic logic by introducing algebraic equations into modalities. Algebraic transition systems are embedded in modalities of logic formulas which specify properties of algebraic transition systems. The semantics of modalities and formulas is defined with solutions of algebraic equations. A proof system for this logic is constructed to verify properties of algebraic transition systems. The proof system combines with inference rules decision procedures on the theory of polynomial ideals to reduce a proof-search problem to an algebraic computation problem. The proof system proves to be sound but inherently incomplete. Finally, a typical example illustrates that reasoning about algebraic transition systems with our approach is feasible.

scholarly journals Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

2018 ◽  
Author(s):  
Jan Elffers ◽  
Jesús Giráldez-Cru ◽  
Stephan Gocht ◽  
Jakob Nordström ◽  
Laurent Simon
Keyword(s):  
Systematic Study ◽  
Boolean Satisfiability ◽  
Proof System ◽  
Sat Solvers ◽  
Proof Search ◽  
Wide Range ◽  
Clause Learning ◽  
Resolution Proof ◽  
Shed Light

Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.

scholarly journals RPO semantics for mobile ambients

2014 ◽  
Vol 24 (4) ◽  
Author(s):  
FILIPPO BONCHI ◽  
FABIO GADDUCCI ◽  
GIACOMA VALENTINA MONREALE
Keyword(s):  
Operational Semantics ◽  
Inference Rules ◽  
Synthesis Mechanism ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Process Calculi ◽  
Mobile Ambients

In this paper we focus on the synthesis of labelled transition systems (LTSs) for process calculi using Mobile Ambients (MAs) as a testbed. Our proposal is based on a graphical encoding: a process is mapped into a graph equipped with interfaces such that the denotation is fully abstract with respect to the standard structural congruence. Graphs with interfaces are amenable to the synthesis mechanism based on borrowed contexts (BCs), which is an instance of relative pushouts (RPOs). The BC mechanism allows the effective construction of an LTS that has graphs with interfaces as states and labels, and such that the associated bisimilarity is a congruence. We focus here on the analysis of an LTS over processes as graphs with interfaces: we use the LTS on graphs to recover an LTS directly defined over the structure of MA processes and define a set of SOS inference rules capturing the same operational semantics.

Modeling legal conflict resolution based on dynamic logic

2020 ◽  
Author(s):  
Fengkui Ju ◽  
Karl Nygren ◽  
Tianwen Xu
Keyword(s):  
Conflict Resolution ◽  
Legal Status ◽  
Dynamic Logic ◽  
Legal Systems ◽  
Transition Systems ◽  
Legal Norms

Abstract Conflicts between legal norms are common in reality. In many legislations, legal conflicts between norms are resolved by applying ordered principles. This work presents a formalization of the conflict resolution mechanism and introduces action legal logic ($\textsf{ALL}$) to reason about the normative consequences of possibly conflicting legal systems. The semantics of $\textsf{ALL}$ is explicitly based on legal systems consisting of norms and ordered principles. Legal systems specify the legal status of transitions in transition systems and the language of $\textsf{ALL}$ describes the legal status of paths in transition systems. The formalization is used to study abstract revisions of legal systems. The expressivity of $\textsf{ALL}$ is studied and its completeness is proved.

A Hierarchy of System Descriptions via Atomic Linear Refinement

1992 ◽  
Vol 16 (3-4) ◽  
pp. 289-336
Author(s):  
Roberto Gorrieri
Keyword(s):  
Proof System ◽  
Weak Equivalence ◽  
Levels Of Abstraction ◽  
Complete Proof ◽  
Transition Systems ◽  
Action Refinement ◽  
Atomic Action ◽  
Description Languages ◽  
Different Levels

The problem of relating system descriptions at different levels of abstraction is studied in the field of Process Description Languages, following the so-called interleaving approach. Since we believe that several different languages should be used profitably during the hierarchical specification process, we investigate the problem of implementing a calculus into another one. As a case study, we introduce a pair of languages which will be increasingly enriched. The basic languages are sequential and nondeterministic; their first enrichment is obtained by adding an operator for asynchrony; then also communication is added, and finally restriction is dealt with. For each pair, the latter language extends the former with atomicity, obtained by adding to the signature of the former an operator of strong prefixing that makes atomic the execution of a sequence of actions. The two languages are intended to be a specification and an implementation language, respectively. To directly relate them, a mapping, called atomic linear refinement, is introduced from actions of the former to atomic sequences (i.e. sequences of actions built with strong prefixing) of the latter. An atomic linear refinement can be homomorphically extended to become a mapping among process terms of the two languages and thus also among the states of their associated transition systems. A notion of implementation, based on a sort of bisimulation (parametric with respect to an atomic action refinement), relates processes of the two languages. Given a specification process p and an atomic action refinement ρ, the refined process ρ(p) is proved to be an implementation of p. Moreover, a complete proof system for strong and weak equivalence are presented for both languages (and thus also for the operator of strong prefixing) and proved consistent with respect to refinement: if p and ρ are congruent processes of the specification language, then ρ(p) and ρ(q) are congruent, too.

scholarly journals A Modal Characterisation of Distributed Bisimulation

1991 ◽  
Vol 20 (347) ◽  
Author(s):  
Søren Christensen
Keyword(s):  
Special Kind ◽  
The Other ◽  
Proof System ◽  
Small Subset ◽  
Parallel Composition ◽  
Inference Rules ◽  
Bisimulation Equivalence ◽  
Distributed Bisimulation

In this paper we consider the distributed bisimulation equivalence defined by Hennessy and Castellani and later developed by Castellani. We present a logic in the style of Hennessy-Milner logic to charaterize the equivalence, i.e. we seek a logic such that whenever two processes are distributed bisimulation equivalent, they satisfy the same set of formulae and vice versa. Furthermore, for a small subset of CCS we provide a proof system which is shown to be sound and complete. The proof system is structural both in the structure of formulae and in the structure of processes. For the case of parallel composition of processes we present inference rules defined via a new combinator introduced. The combinator in question is left merge, a special kind of parallel composition in which the left operand has precedence over the other and must perform the first action observed.

scholarly journals Reducing the Problem of Minimax Control of Linear non-Stationary Systems to a - Robust One by the Way of Dynamic Game

2020 ◽  
pp. 143-162
Author(s):  
Oleksij Lobok ◽  
◽  
Boris Goncharenko ◽  
Larisa Vihrova ◽  
◽  
...  
Keyword(s):  
Optimal Control ◽  
Control Problem ◽  
Initial Conditions ◽  
Dynamic Game ◽  
Quality Criterion ◽  
Necessary Condition ◽  
Search Problem ◽  
Algebraic Equations ◽  
Initial State ◽  
Minimax Control

The problem of synthesis of minimax control for the dynamic, described by the linear system of differential equations (taking into account the state, controls, perturbations and initial conditions, with the given equation of observation inclusive) of objects functioning in accordance with the integral-quadratic quality criterion in uncertainty is solved in the work. External perturbations, errors, and initial conditions were assumed to belong to a number of uncertainties. The task of finding optimal control in the form of a feedback object that minimizes the performance criterion is presented in the form of a minimum maximal uncertainty control problem. In the absence of ready-made solution paths, this problem is reduced to a -control problem under the most unfavorable disturbances, and in addition to a dynamic game problem with zero sum and a certain price for the game, and a strategy for solving it is proposed that offers a way to new results. The problem of finding the optimal control and the initial state that maximize the quality criterion is considered in the framework of the optimization problem solved by the Lagrange multiplier method after introducing the auxiliary scalar function, the Hamiltonian. It is shown that to find the maximum value of the criterion, either the necessary condition of the extremum of the first kind can be used, which depends on the ratio of the first variation of the criterion and the first variations of the control vectors and the initial state, or also the necessary condition of the extremum of the second kind, which depends on the sign of the second variation. For the first and second variations, formulas are given that can be used for calculations. It is suggested to solve the control search problem in two steps: search for an intermediate solution at fixed values of control vectors and errors, and then search for final optimal control. Consideration is also given to solving -optimal control for infinite control time with respect to the signal from the compensator output, as well as solving the corresponding Riccati matrix algebraic equations.

Structured pigeonhole principle, search problems and hard tautologies

2005 ◽  
Vol 70 (2) ◽  
pp. 619-630 ◽  
Author(s):  
Jan Krajíček
Keyword(s):  
Proof Complexity ◽  
Proof System ◽  
Search Problem ◽  
Ramsey Property ◽  
Relational Structures ◽  
Proof Systems ◽  
Polynomial Size ◽  
Hashing Function ◽  
The Universe ◽  
Study Behaviour

AbstractWe consider exponentially large finite relational structures (with the universe {0, 1}n) whose basic relations are computed by polynomial size (nO(1)) circuits. We study behaviour of such structures when pulled back by P/poly maps to a bigger or to a smaller universe. In particular, we prove that:1. If there exists a P/poly map g: {0, 1}n → {0, 1}m, n < m, iterable for a proof system then a tautology (independent of g) expressing that a particular size n set is dominating in a size 2n tournament is hard for the proof system.2. The search problem WPHP. decoding RSA or finding a collision in a hashing function can be reduced to finding a size m homogeneous subgraph in a size 22m graph.Further we reduce the proof complexity of a concrete tautology (expressing a Ramsey property of a graph) in strong systems to the complexity of implicit proofs of implicit formulas in weak proof systems.

Sign in / Sign up

Export Citation Format

Share Document