Comments on "Stability of time-delay systems"

It is shown that a theorem of stability of time-delay system is not valid for some conditions. An alternative proof is given for the theorem which reveals the conditions for which stability can be determined.     

Comments on "A training rule which guarantees finite-region stability for a class of closed-loop neural-network control systems" [with reply].

In the above paper by Kuntanapreeda-Fullmer (ibid., vol.7, no.3 (1996)) a training method for a neural-network control system which guarantees local closed-loop stability is proposed based on a Lyapunov function and a modified standard backpropagation training rule. In this letter, we show that the proof of Proposition 1 and the proposed stability condition as training constraints are not correct and therefore that the stability of the neural-network control system is not quite right. We suggest a modified version of the proposition with its proof and comment on another problem of the paper. In reply, Kuntanapreeda-Fullmer maintain the proof in the original paper is correct. Rather than identifying an error, they believe Park et al. have made a significant extension of the proof for application to stable online training networks.     

Comments on "Parameter identification and control of linear discrete-time systems"

A new proof of convergence of the stochastic approximation algorithm for parameter identification of closed-loop linear discrete-time control systems is proposed. This algorithm relates very effectively in terms of a sufficient condition the stability properties of the closed-loop system with the convergence of the identification algorithms, which were previously treated independently.     

Comments on "Exact control of linear systems with multiple control"

This note is concerned with piecewise constant controls. In order to supplement the above-mentioned paper sufficient conditions for the existence of a piecewise constant control are provided. Moreover, although for ann-dimensional control system the switching times for the piecewise constant control cannot he chosen arbitrarily, it is shown that the switching times can be chosen as close as we wish to any preassigned collection ofntime points. The proof of the main result is constructive and it provides an algorithm for the design of a piecewise constant control.     

Strongly simulation-extractable leakage-resilient NIZK

This paper defines strongly simulation-extractable (sSE) leakage resiliency (LR), which is a new notion for non-interactive zero-knowledge (NIZK) proof system. For an sSE-NIZK proof system, there exists a probabilistic polynomial-time extractor that can always extract a correct witness from any valid proof generated by the adversary, who can obtain proofs of true statements previously given by the simulator. The proof generated by the adversary may depend on a statement–tag pair which has already been used by the simulator. Furthermore, if the adversary can also learn leakage on witnesses and randomness which can explain the proofs generated by the simulator, then the sSE-NIZK proof system is said to satisfy the property of LR. In ASIACRYPT 2010, Dodis, Haralambiev, López-Alt, and Wichs proposed the definitions of true simulation-extractable (tSE) NIZK proof system and sSE-NIZK proof system and gave their constructions. The tSE-NIZK proof system is the same as the sSE-NIZK proof system except that the proof generated by the adversary cannot depend on a statement–tag pair which was used by the simulator. As an extension of the tSE-NIZK proof system, Garg, Jain, and Sahai defined a new notion for NIZK proof system called tSE-LR in CRYPTO 2011 and provided the construction of tSE-LR-NIZK proof system. We extend the notion of tSE-LR-NIZK proof system and construct it by improving the construction of tSE-LR-NIZK proof system. An sSE-LR-NIZK proof system is applicable to construct a fully leakage-resilient signature scheme which is strongly existentially unforgeable, while a tSE-LR-NIZK proof system is applicable to construct one which just satisfies the weak existentially unforgeability. Although there has already been a great deal of research proposed for cryptographic primitives in the leakage models, as far as we know, this is the first fully leakage-resilient signature scheme that is strongly existentially unforgeable.     

Comments on "On structural controllability theorem"

In the above mentioned paper, Mayeda gave an elegant proof to the structural controllability theorem. This note suggests further simplification of that proof using graph-theoretic interpretation of some determinants.     

PVS#: Streamlined Tacticals for PVS

The semantics of a proof language relies on the representation of the state of a proof after a logical rule has been applied. This information, which is usually meaningless from a logical point of view, is fundamental to describe the control mechanism of the proof search provided by the language. In this paper, we present a monadic datatype to represent the state information of a proof and we illustrate its use in the PVS theorem prover. We show how this representation can be used to design a new set of powerful tacticals for PVS, called PVS#, that have a simpler and clearer semantics compared to the semantics of standard PVS tacticals.     

Remarks on a recent paper on the "no free lunch" theorems

This note discusses the recent paper "Some technical remarks on the proof of the no free lunch theorem" by Koppen (2000). In that paper, some technical issues related to the formal proof of the no free lunch (NFL) theorem for search were given by Wolpert and Macready (1995, 1997). The present authors explore the issues raised in that paper including the presentation of a simpler version of the NFL proof in accord with a suggestion made explicitly by Koppen (2000) and implicitly by Wolpert and Macready (1997). They also includes the correction of an incorrect claim made by Koppen (2000) of a limitation of the NFL theorem. Finally, some thoughts on future research directions for research into algorithm performance are given.     

Comments on "Cooperative games and vector-valued criteria problems"

A theorem in the above paper,[1] giving sufficient conditions for the local Pareto optimality, is shown to be incorrect by a counter-example and a revision of its proof. Moreover, an alternative formulation of this theorem is suggested.     

哈希证明系统及应用研究

哈希证明系统在2002年欧密会上由Cramcr和Shoup首次提出。哈希证明系统的概念自提出以来得到广泛 研究,目前已有多个修改版本。“投影性”和“平滑性”是哈希证明系统的两个重要特性,正是由于这两个特性使得哈希 证明系统除了用于设计CCA安全的公钥加密体制之外,还广泛应用于各种安全协议设计,比如:基于口令认证的密钥 交换协议、不经意传输协议、可否认的认证协议、零知识证明协议和承诺协议等。介绍了哈希证明系统及其变形的各 种定义,分析了定义之间的派生关系和安全级别关系,并讨论了哈希证明系统在密码学中的应用.     

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.     

Comments on "Decoupled decomposition of the Riccati equation"

The aim of this paper is to point out that a sufficient condition in the existence theorem of the solution of Riccati equations obtained in the above paper is also necessary. Our proof of the theorem inclusive of the sufficiency is more perspicuous although it is the same in essence as that in the above paper.     

Mechanically verifying concurrent programs with the Boyer-Mooreprover

A proof system suitable for the mechanical verification of concurrent programs is described. This proof system is based on Unity, and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an operational semantics of the transition system model of concurrency. Proof rules are simply theorems of this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the underlying logic. Since this proof system essentially encodes Unity in another sound logic, and this encoding has been mechanically verified, this encoding proves the soundness of this formalization of Unity. This proof system has been mechanically verified by the Boyer-Moore prover. This proof system has been used to mechanically verify the correctness of a distributed algorithm that computes the minimum node value in a tree     

Focusing and polarization in linear,intuitionistic, and classical logics

A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard’s LC and LU proof systems.     

Proving Properties of Dynamic Process Networks

We present the first compositional proof system for checking processes against formulas in the modalμ-calculus which is capable of handling dynamic process networks. The proof system is obtained in a systematic way from the operational semantics of the underlying process algebra. A non-trivial proof example is given, and the proof system is shown to be sound in general, and complete for finite-state processes.     

Comments on "Adaptive controller designs for robot manipulator systems using Lyapunov direct method"

The asymptotic stability result claimed in the paper is modified. Ihe proof shown there is also improved.     

Comments on "Inversion of multivariable linear systems"

The purpose is to give a simple algebraic proof to the necessary part of the criterion of functional reproducibility of multivariable linear systems given by Silverman and to incorporate a slight correction to his criterion. Furthermore, the criteria of the functional reproducibility of Silverman and Sain and Massey [1] are shown to be equivalent.     

A Comparison of Mizar and Isar

The mathematical proof checker Mizar by Andrzej Trybulec uses a proof input language that is much more readable than the input languages of most other proof assistants. This system also differs in many other respects from most current systems. John Harrison has shown that one can have a Mizar mode on top of a tactical prover, allowing one to combine a mathematical proof language with other styles of proof checking. Currently the only fully developed Mizar mode in this style is the Isar proof language for the Isabelle theorem prover. In fact the Isar language has become the official input language to the Isabelle system, even though many users still use its low-level tactical part only. In this paper we compare Mizar and Isar. A small example, Euclid's proof of the existence of infinitely many primes, is shown in both systems. We also include slightly higher-level views of formal proof sketches. Moreover, a list of differences between Mizar and Isar is presented, highlighting the strengths of both systems from the perspective of end-users. Finally, we point out some key differences of the internal mechanisms of structured proof processing in either system.     

Derandomized Parallel Repetition via Structured PCPs

A PCP is a proof system for NP in which the proof can be checked by a probabilistic verifier. The verifier is only allowed to read a very small portion of the proof and in return is allowed to err with some bounded probability. The probability that the verifier accepts a proof of a false claim is called the soundness error and is an important parameter of a PCP system that one seeks to minimize. Constructing PCPs with subconstant soundness error and, at the same time, a minimal number of queries into the proof (namely two) is especially important due to applications for inapproximability.     

基于Isabelle的证明信息系统设计

Isabelle定理证明器中的证明步骤和证明状态是非常具有参考价值的证明信息。然而目前没有工具可以有效管理这些信息。本文给出一个基于Isabelle的信息系统设计方案。利用该系统的实现,用户可以提取、保存和搜索这两种证明信息。