scholarly journals A logical method for the synthesis of periodic trajectory in a binary dynamical system

2021 ◽  
Author(s):  
G.A. Oparin ◽  
V.G. Bogdanova ◽  
A.A. Pashinin
Keyword(s):  
Dynamical System ◽  
Periodic Trajectory ◽  
Software Implementation ◽  
Boolean Formula ◽  
Dynamical Models ◽  
Composite Service ◽  
Parametric Synthesis ◽  
Quantified Boolean Formula ◽  
Logical Method ◽  
One Step

A logic method for structural-parametric synthesis of a binary dynamical system with a given periodic trajectory is proposed. This method provides a constructive solution for the considered problem. The attraction region of such a trajectory must coincide with a given subset of the state space. An additional constraint sets the acceptable time for reaching this trajectory from its attraction region. As admissible structures for dynamical models of the synthesis, we consider the following systems: linear systems, systems with the disjunctive and conjunctive right sides. All conditions of the problem are written in the form of a quantified Boolean formula with subsequent verification of its truth using a specialized solver, which gives values of the required parameters of the dynamical model. The software implementation of the proposed method in the form of a composite service is presented. All stages of the parametric synthesis of a Boolean network based on the proposed method are demonstrated in the example of a one-step linear system.

GALTON'S QUINCUNX: RANDOM WALK OR CHAOS?

2007 ◽  
Vol 17 (12) ◽  
pp. 4463-4469 ◽  
Author(s):  
KEVIN JUDD
Keyword(s):  
Dynamical System ◽  
Random Walk ◽  
Central Limit Theorem ◽  
Limit Theorem ◽  
Mechanical Device ◽  
Dynamical Models ◽  
The Central Limit Theorem ◽  
Random Events ◽  
Low Dimensional ◽  
Deterministic Dynamical System

In 1873 Francis Galton had constructed a simple mechanical device where a ball is dropped vertically through a harrow of pins that deflect the ball sideways as it falls. Galton called the device a quincunx, although today it is usually referred to as a Galton board. Statisticians often employ (conceptually, if not physically) the quincunx to illustrate random walks and the central limit theorem. In particular, how a Binomial or Gaussian distribution results from the accumulation of independent random events, that is, the collisions in the case of the quincunx. But how valid is the assumption of "independent random events" made by Galton and countless subsequent statisticians? This paper presents evidence that this assumption is almost certainly not valid and that the quincunx has the richer, more predictable qualities of a low-dimensional deterministic dynamical system. To put this observation into a wider context, the result illustrates that statistical modeling assumptions can obscure more informative dynamics. When such dynamical models are employed they will yield better predictions and forecasts.

scholarly journals Investigation of observability property of controlled binary dynamical systems: a logical approach

2021 ◽  
Author(s):  
G.A. Oparin ◽  
V.G. Bogdanova ◽  
A.A. Pashinin
Keyword(s):  
Dynamical Systems ◽  
Binary System ◽  
System Dynamics ◽  
Boolean Model ◽  
Boolean Formula ◽  
Formal Definition ◽  
Applied Logic ◽  
Quantified Boolean Formula ◽  
Logical Specification ◽  
Definition Of

The property of observability of controlled binary dynamical systems is investigated. A formal definition of the property is given in the language of applied logic of predicates with bounded quantifiers of existence and universality. A Boolean model of the property is built in the form of a quantified Boolean formula accordingly to the Boolean constraints method developed by the authors. This formula satisfies both the logical specification of the property and the equations of the binary system dynamics. Aspects of the proposed approach implementation for the study of the observability property are considered. The technology of checking the feasibility of the property using an applied microservice package is demonstrated in several examples.

scholarly journals Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver

2021 ◽  
pp. 433-449
Author(s):  
Randal E. Bryant ◽  
Marijn J. H. Heule
Keyword(s):  
Binary Decision Diagrams ◽  
Boolean Formula ◽  
Decision Diagrams ◽  
Ordered Binary Decision Diagrams ◽  
Binary Decision ◽  
Quantified Boolean Formulas ◽  
Quantified Boolean Formula ◽  
Boolean Formulas ◽  
Time Required

AbstractExisting proof-generating quantified Boolean formula (QBF) solvers must construct a different type of proof depending on whether the formula is false (refutation) or true (satisfaction). We show that a QBF solver based on ordered binary decision diagrams (BDDs) can emit a single dual proof as it operates, supporting either outcome. This form consists of a sequence of equivalence-preserving clause addition and deletion steps in an extended resolution framework. For a false formula, the proof terminates with the empty clause, indicating conflict. For a true one, it terminates with all clauses deleted, indicating tautology. Both the length of the proof and the time required to check it are proportional to the total number of BDD operations performed. We evaluate our solver using a scalable benchmark based on a two-player tiling game.

scholarly journals Stability of the Solar System

1979 ◽  
Vol 81 ◽  
pp. 7-15
Author(s):  
Victor Szebehely
Keyword(s):  
Dynamical System ◽  
Solar System ◽  
Quantitative Measure ◽  
Marginal Stability ◽  
Actual Behavior ◽  
The Sun ◽  
Dynamical Models ◽  
Restricted Problems ◽  
Hill’S Method ◽  
The Stability

This paper reviews the present status of research on the problem of stability of satellite and planetary systems in general. In addition new results concerning the stability of the solar system are described. Hill's method is generalized and related to bifurcation (or catastrophe) theory. The general and the restricted problems of three bodies are used as dynamical models. A quantitative measure of stability is introduced by establishing the differences between the actual behavior of the dynamical system as given today and its critical state. The marginal stability of the lunar orbit is discussed as well as the behavior of the Sun-Jupiter-Saturn system. Numerical values representing the measure of stability of several components of the solar system are given, indicating in the majority of cases bounded behavior.

scholarly journals Compact Tree Encodings for Planning as QBF

2018 ◽  
Vol 21 (62) ◽  
pp. 103-113
Author(s):  
Olivier Gasquet ◽  
Dominique Longin ◽  
Fr´ed´eric Maris ◽  
Pierre R´egnier ◽  
Ma¨el Valais
Keyword(s):  
Artificial Intelligence ◽  
Execution Time ◽  
Boolean Formula ◽  
Benchmark Problems ◽  
Sat Solvers ◽  
Quantified Boolean Formula ◽  
And Performance ◽  
Near Future ◽  
Planning Problems ◽  
Better Than

Considerable improvements in the technology and performance of SAT solvers has made their use possible for the resolution of various problems in artificial intelligence, and among them that of generating plans. Recently, promising Quantified Boolean Formula (QBF) solvers have been developed and we may expect that in a near future they become as efficient as SAT solvers. So, it is interesting to use QBF language that allows us to produce more compact encodings. We present in this article a translation from STRIPS planning problems into quantified propositional formulas. We introduce two new Compact Tree Encodings: CTE-EFA based on Explanatory frame axioms, and CTE-OPEN based on causal links. Then we compare both of them to CTE-NOOP based on No-op Actions proposed in [Cashmore et al. 2012]. In terms of execution time over benchmark problems, CTE-EFA and CTE-OPEN always performed better than CTE-NOOP.

CASCADING RANDOM WALKS

2005 ◽  
Vol 16 (03) ◽  
pp. 599-622 ◽  
Author(s):  
K. SUBRAMANI
Keyword(s):  
Directed Graphs ◽  
Randomized Algorithm ◽  
Conjunctive Normal Form ◽  
Monte Carlo Algorithm ◽  
Linear Ordering ◽  
Boolean Formula ◽  
Quantified Boolean Formula ◽  
Boolean Formulas ◽  
Complete Set ◽  
Time Required

In this paper, we discuss a simple, Monte Carlo algorithm for the problem of checking whether a Quantified Boolean Formula (QBF) in Conjunctive Normal Form (CNF), with at most two literals per clause has a model. The term k-CNF is used to describe boolean formulas in CNF, with at most k literals per clause and the problem of checking whether a given k-CNF formula is satisfiable is called the k-SAT problem. A QBF is a boolean formula, accompanied by a quantifier string which imposes a linear ordering on the variables of that formula. The problem of finding a model for a QBF formula in CNF, with at at most k literals per clause is called the QkSAT problem. The QkSAT problem is PSPACE-complete, for k≥3. However, the Q2SAT problem can be decided in polynomial time; the graph-based procedure, discussed in [1], is the first such algorithm for this problem. This procedure requires the construction of a global implication graph, corresponding to the input formula and searching for certain paths in this graph. Hence the complete set of clauses must be part of the input. We propose an incremental, randomized approach for the Q2SAT problem that is essentially local in nature, in that the complete clausal set need not be provided at any time, in the presence of a verifier. We show that the randomized algorithm can be analyzed as a one-dimensional random walk, with one reflecting barrier and one absorbing barrier. On a Q2SAT instance with m clauses on n variables, our coin-flipping algorithm runs in time O(n2 · V(m, n)), where V(m, n) is the time required to verify that a given model satisfies the formula. Additionally, if the instance is satisfiable, the probability that our algorithm fails to find a model is less than one half. The design and analysis of a randomized algorithm for a problem, is important from both the theoretical and the practical perspectives. Randomized approaches tend to be simple and elegant, thereby making the process of checking correctness, effortless as well. The randomized approach discussed in this paper lays the groundwork for analyzing a number of problems related to 2CNF formulas and directed graphs. We remark that our work in this paper is the first randomized algorithm for a class of QBFs.

Disentangling dynamics, computation, and cognition

1998 ◽  
Vol 21 (5) ◽  
pp. 654-661 ◽  
Author(s):  
Tim van Gelder
Keyword(s):  
Dynamical System ◽  
Cognitive Science ◽  
Digital Computer ◽  
Multiple Realizability ◽  
Dynamical Models ◽  
Target Article ◽  
Ontological Claim ◽  
Qualitative Structure ◽  
Dynamical Hypothesis

The nature of the dynamical hypothesis in cognitive science (the DH) is further clarified in responding to various criticisms and objections raised in commentaries. Major topics addressed include the definitions of “dynamical system” and “digital computer”; the DH as Law of Qualitative Structure; the DH as an ontological claim; the multiple-realizability of dynamical models; the level at which the DH is formulated; the nature of dynamics; the role of representations in dynamical cognitive science; the falsifiability of the DH; the extent to which the DH is open; the role of temporal and implementation considerations; and the novelty or importance of the DH. The basic formulation and defense of the DH in the target article survives intact, though some refinements are recommended.

Sign in / Sign up

Export Citation Format

Share Document