Exogenous Probabilistic Computation Tree Logic

We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non–deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so–called quantum one–time pad.     

Practical Reflection for Sequent Logics

It is well-known that adding reflective reasoning can tremendously increase the power of a proof assistant. In order for this theoretical increase of power to become accessible to users in practice, the proof assistant needs to provide a great deal of infrastructure to support reflective reasoning. In this paper we explore the problem of creating a practical implementation of such a support layer.Our implementation takes a specification of a logical theory (which is identical to how it would be specified if we were simply going to reason within this logical theory, instead of reflecting it) and automatically generates the necessary definitions, lemmas, and proofs that are needed to enable the reflected meta-reasoning in the provided theory.One of the key features of our approach is that the structure of a logic is preserved when it is reflected. In particular, all variables, including meta-variables, are preserved in the reflected representation. This also allows the preservation of proof automation—there is a structure-preserving one-to-one map from proof steps in the original logic to proof step in the reflected logic.To enable reasoning about terms with sequent context variables, we develop a principle for context induction, called teleportation.This work is fully implemented in the MetaPRL theorem prover.     

Deadlock and starvation free reentrant readers-writers: A case study combining model checking with theorem proving

The classic readers-writers problem has been extensively studied. This holds to a lesser degree for the reentrant version, where it is allowed to nest locking actions. Such nesting is useful when a library is created with various procedures each starting and ending with a lock operation. Allowing nesting makes it possible for these procedures to call each other.We considered an existing widely used industrial implementation of the reentrant readers-writers problem. Staying close to the original code, we modelled and analyzed it using a model checker resulting in the detection of a serious error: a possible deadlock situation. The model was improved and checked satisfactorily for a fixed number of processes. To achieve a correctness result for an arbitrary number of processes the model was converted to a specification that was proven with a theorem prover. Furthermore, we studied starvation. Using model checking we found a starvation problem. We have fixed the problem and checked the solution. Combining model checking with theorem proving appeared to be very effective in reducing the time of the verification process.     

Virtual Organizations in Arigatoni

Arigatoni is a lightweight overlay network that deploys the Global Computing Paradigm over the Internet. Communication for over the behavioral units of the overlay is performed by a simple resource discovery protocol (RDP). Basic Global Computers Units (GC) can communicate by first registering to a brokering service and then by mutually asking and offering services.Colonies and communities are the main entities in the model. A colony is a simple virtual organization composed by exactly one leader and some set (possibly empty) of individuals. A community is a raw set of colonies and global computers (think it as a soup of colonies and global computer without a leader).We present an operational semantics via a labeled transition system, that describes the main operations necessary in the Arigatoni model to perform leader negotiation, joining/leaving a colony, linking two colonies and moving one GC from one colony to another. Our formalization results to be adequate w.r.t. the algorithm performing peer logging/delogging and colony aggregation.     

Control of single-sector economy over a finite time interval with allowance for employer consumption

The problem of optimal control of a single-sector economics over a finite time interval was studied for the class of the linear uniform production functions in terms of the criterion for maximum employer consumption under exponential growth of the manpower resources. Solution was obtained in the form of the “turnpike theorem.” Its properties were considered. The results obtained were specified for the case of the Cobb-Douglas production function.     

A Petri Net Semantics of a Simple Process Algebra for Mobility

In this paper, we propose a structural translation of terms from a simple variant of the Klaim process algebra into behaviourally equivalent finite high level Petri nets. This yields a formal semantics for mobility allowing one to deal directly with concurrency and causality.     

Security analysis of the SCO-family using key schedules

The COS-based ciphers SCO-1, SCO-2 and SCO-3 (called the SCO-family) have been designed to improve the security of DDP-based ciphers which are all broken by related-key attacks. In this paper we show that the SCO-family is still vulnerable to related-key attacks: we present related-key differential attacks on a full-round SCO-1, a full-round SCO-2 and an 11-round reduced SCO-3, respectively. The attack on SCO-1 requires 2⁶¹ related-key chosen ciphertexts and 2^120.59 full-round SCO-1 decryptions. For the attack on SCO-2, we require 2⁵⁹ related-key chosen plaintexts and 2^118.42 full-round SCO-2 encryptions, and the 11-round attack on SCO-3 works with 2⁵⁸ related-key chosen plaintexts and 2^117.54 11-round SCO-3 encryptions. This work is the first known cryptanalytic results on the SCO-family.     

Perfect Parallel Repetition Theorem for Quantum Xor Proof Systems

We consider a class of two-prover interactive proof systems where each prover returns a single bit to the verifier and the verifier’s verdict is a function of the XOR of the two bits received. We show that, when the provers are allowed to coordinate their behavior using a shared entangled quantum state, a perfect parallel repetition theorem holds in the following sense. The prover’s optimal success probability for simultaneously playing a collection of XOR proof systems is exactly the product of the individual optimal success probabilities. This property is remarkable in view of the fact that, in the classical case (where the provers can only utilize classical information), it does not hold. The theorem is proved by analyzing parities of XOR proof systems using semidefinite programming techniques, which we then relate to parallel repetitions of XOR games via Fourier analysis.      

Local search of orthogonal packings using the lower bounds

Consideration was given to the problem of packing the rectangular half-infinite strip. It was suggested to solve it using a one-point evolutionary algorithm with search of the best solution in the neighborhood of the local lower bound. Proposed was an algorithm to construct this neighborhood including the packings obtained by solving a special problem of one-dimensional cutting. Its solution was shown to be the local lower bound in the considered neighborhood. An improved global lower bound was proposed. The results of numerical modeling were presented. The record value obtained was compared with the global bounds.     

Concurrent Java Test Generation as a Search Problem

A Random test generator generates executable tests together with their expected results. In the form of a noise-maker, it seeds the program with conditional scheduling primitives (such as yield()) that may cause context switches. As a result different interleavings are potentially produced in different executions of the program. Determining a-priori the set of seeded locations required for a bug to manifest itself is rarely possible.This work proposes to reformulate random test generation of concurrent Java programs as a search problem. Hence, it allows applying a set of well known search techniques from the domain of AI to the input space of the test generator. By iteratively refining the input parameters fed to the test generator, the search process creates testing scenarios (i.e. interleavings) that maximizes predefined objective functions. We develop geneticFinder, a noise-maker that uses a genetic algorithm as a search method. We demonstrate our approach by maximizing two objective functions: the high manifestation rate of concurrent bugs and the exporting of a high degree of debugging information to the user. Experimental results show our approach is effective.     

Construction of invariant ellipsoids in the stabilization problem for a wheeled robot following a curvilinear path

The synthesis control problem for the plane motion of a wheeled robot is studied. The goal of the control is to bring the robot to an assigned curvilinear trajectory and to stabilize its motion along it in the presence of phase and control constraints. For a synthesized control law, invariant ellipsoids—quadratic approximations of the attraction domains of the target trajectory—are constructed, which allow one to check in the course of the robot motion whether the control law can stabilize motion along the current trajectory segment. To take into account constraints on the control, methods of absolute stability theory are applied. The construction of the invariant ellipsoids reduces to solving a system of linear matrix inequalities.     

Local and semiglobal stabilization in a cascade with delay

Consideration is given to the problem of stability and stabilization for a system of differential equations with delay of a “cascade” structure. Sufficient conditions for local asymptotic stability as well as “semiglobal” stabilization for a cascade with a linear subsystem are obtained.     

Optimization of boundary control at one end of a string in the presence of a model nonlocal condition

The paper is devoted to problems of optimal boundary control of string vibrations under nonlocal conditions that relate values of string displacement or its derivative at the boundary point with their values at the interior point. The solutions for all problems of boundary control are obtained in explicit analytic form.     

Criteria of resonance origin in a single-circuit control system with saturation

Studies are made of forced periodic oscillations in a single-circuit control system with a parameter, the dynamics of which is described by resonance equations in the linear approximation. Criteria are suggested of the origin of resonance that is understood as an increase to infinity of the amplitude of forced oscillations in the approximation of the parameter to certain critical values. The principal results relate to the case when answers are defined by bounded nonlinearities of the order of a constant; the summands that decrease to zero are of no importance.     

Lambert function and some problems of control in a Lancaster model

A special class of controls in a Lancaster model of a battle of two armies is studied. It was shown that important characteristics of the dynamics of the battle can be estimated by a Lambert function.     

Dynamic features of flexible spacecraft control in process of its transformation into a large space structure

Consideration was given to dynamics of angular motion control of the flexible spacecraft reconstructed into a large space structure. In formal terms, this transformation lies in gradual reduction of the constructive rigidity to small values giving rise to low-frequency ( $ \tilde f Consideration was given to dynamics of angular motion control of the flexible spacecraft reconstructed into a large space structure. In formal terms, this transformation lies in gradual reduction of the constructive rigidity to small values giving rise to low-frequency ( ≤ 0.05 Hz) oscillations which represent one of the attributes of the class of large space structures. The existing quantitative definition of the large space structure was specified. It was demonstrated that as the frequencies of structure’s elastic oscillations approach those of the control of object “rigid” motion, a new kind of interrelations between the motions of both types, the so-called “capture” of the controller frequency by that of the elastic oscillations, arises which impairs control efficiency to the point of losing system stability. Analytical (for the linear control systems) and computer-aided (for the discrete systems) methods for determination of the boundaries separating the two qualitatively different forms of existence of the transformed elastic object were proposed. Some results of computer simulation of the orientation control of variable objects such as flexible spacecraft and large space structure were presented. Original Russian Text ? I.N. Krutova, V.M. Sukhanov, 2008, published in Avtomatika i Telemekhanika, 2008, No. 5, pp. 41–56. This work was supported by the Russian Foundation for Basic Research, project no. 05-08-18175.     

Identification of frequency of a shifted sinusoidal signal

The article deals with the issue of identification of an unknown frequency of a shifted sinusoidal signal y(t) = σ ₀ + σ sin(ωt + ?). A new approach taken to estimate the frequency of a shifted sinusoidal signal is suggested, which is a robust approach relative to undetermined disturbances present in the measurement of a useful signal. In contrast to known analogs, the given approach permits controlling the time of estimation of the unknown frequency ω. The dimension of the identification algorithm suggested is less than that of known analogs.     

On-the-fly Workload Prediction and Redistribution in the Distributed Timed Model Checker Zeus

In this work we present the on-the-fly workload prediction and redistribution techniques used in Zeus [Braberman, V., A. Olivero and F. Schapachnik, Zeus: A distributed timed model checker based on kronos, in: Workshop on Parallel and Distributed Model Checking, affiliated to CONCUR 2002 (13^th International Conference on Concurrency Theory), ENTCS 68 (2002), Braberman, V., A. Olivero and F. Schapachnik, Issues in Distributed Model-Checking of Timed Automata: building zeus, to appear in International Journal of Software Tools for Technology Transfer (2004)], a Distributed Model Checker that evolves from the tool Kronos [Daws, C., A. Olivero, S. Tripakis and S. Yovine, The Tool KRONOS, in: Proceedings of Hybrid Systems III, LNCS 1066 (1996), pp. 208–219].After reviewing why it is so hard to have good speedups in distributed timed model checking, we present the methods used to get promising results when verifying reachability properties over timed automata [Alur, R. and D. L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994) 183–235].     

A verified Common Lisp implementation of Buchberger’s algorithm in ACL2

In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort.