A practical approach to model checking Duration Calculus using Presburger Arithmetic

This paper investigates the feasibility of reducing a model-checking problem K???? for discrete time Duration Calculus to the decision problem for Presburger Arithmetic. Theoretical results point at severe limitations of this approach: (1) the reduction in Fränzle and Hansen (Int J Softw Inform 3(2–3):171–196, 2009) produces Presburger formulas whose sizes grow exponentially in the chop-depth of ?, where chop is an interval modality originating from Moszkowski (IEEE Comput 18(2):10–19, 1985), and (2) the decision problem for Presburger Arithmetic has a double exponential lower bound and a triple exponential upper bound. The generated Presburger formulas have a rich Boolean structure, many quantifiers and quantifier alternations. Such formulas are simplified using so-called guarded formulas, where a guard provides a context used to simplify the rest of the formula. A normal form for guarded formulas supports global effects of local simplifications. Combined with quantifier-elimination techniques, this normalization gives significant reductions in formula sizes and in the number of quantifiers. As an example, we solve a configuration problem using the SMT-solver Z3 as backend. Benefits and the current limits of the approach are illustrated by a family of examples.     

Tractable Fragments of Presburger Arithmetic

In this paper we introduce a problem called Quantified Integer Programming, which generalizes the Quantified Satisfiability problem (QSAT). In a Quantified Integer Program (QIP) the program variables can assume arbitrary integral values, as opposed to the boolean values that are assumed by the variables of an instance of QSAT. QIPs naturally represent two-person integer matrix games. The Quantified Integer Programming problem is PSPACE-hard in general, since the QSAT problem is PSPACE-complete. Quantified Integer Programming can be thought of as a restriction of Presburger Arithmetic, in that we allow only conjunctions of linear inequalities. We focus on analyzing various special cases of the general problem, with a view to discovering subclasses that are tractable. Subclasses of the general QIP problem are obtained by restricting either the constraint matrix or quantifier specification or both. We show that if the constraint matrix is totally unimodular, the problem of deciding a QIP can be solved in polynomial time. We also establish the computational complexities of Oblivious strategy games and Clairvoyant strategy games.     

Generic Complexity of Presburger Arithmetic

Fischer and Rabin proved in (Proceedings of the SIAM-AMS Symposium in Applied Mathematics, vol. 7, pp. 27–41, 1974) that the decision problem for Presburger Arithmetic has at least double exponential worst-case complexity (for deterministic and for nondeterministic Turing machines). In Kapovich et al. (J. Algebra 264(2):665–694, 2003) a theory of generic-case complexity was developed, where algorithmic problems are studied on “most” inputs instead of set of all inputs. A question rises about existing of more efficient (say, polynomial) generic algorithm deciding Presburger Arithmetic on a set of closed formulas of asymptotic density 1. We prove in this paper that there is not an exponential generic decision algorithm working correctly on an input set of asymptotic density exponentially converging to 1 (so-called strongly generic sets).     

A Sequent Calculus for Subtyping Polymorphic Types

We present two complete systems for polymorphic types with sub- typing. One system is in the style of natural deduction, while another is a Gentzen-style sequent calculus system. We prove several meta- mathematical properties for these systems including cut elimination, subject reduction, coherence, and decidability of type reconstruction. Following the approach by J. Mitchell, the sequents are given a simple semantics using logical relations over applicative structures. The systems are complete with respect to this semantics. The logic which emerges from this paper can be seen as a successor to the original Hilbert style system proposed by J. Mitchell in 1988, and to the “half way” sequent calculus of G. Longo, K. Milsted, and S. Soloviev proposed in 1995.     

Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols

We study a class of extended automata defined by guarded commands over Presburger arithmetic with uninterpreted functions. On the theoretical side, we show that the bounded reachability problem is decidable in this model. On the practical side, the class is useful for modeling programs with unbounded data structures, and the reachability procedure can be used for symbolic simulation, testing, and verification.     

A 222pn upper bound on the complexity of Presburger Arithmetic

The decision problem for the theory of integers under addition, or “Presburger Arithmetic,” is proved to be elementary recursive in the sense of Kalmar. More precisely, it is proved that a quantifier elimination decision procedure for this theory due to Cooper determines, for any n, the truth of any sentence of length n within deterministic time 2^22pn for some constant p > 1. This upper bound is approximately one exponential higher than the best known lower bound on nondeterministic time. Since it seems to cost one exponential to simulate a nondeterministic algorithm with a deterministic one, it may not be possible to significantly improve either bound.     

An Algorithmic Toolbox for Network Calculus

Network calculus offers powerful tools to analyze the performances in communication networks, in particular to obtain deterministic bounds. This theory is based on a strong mathematical ground, notably by the use of (min,+) algebra. However, the algorithmic aspects of this theory have not been much addressed yet. This paper is an attempt to provide some efficient algorithms implementing network calculus operations for some classical functions. Some functions which are often used are the piecewise affine functions which ultimately have a constant growth. As a first step towards algorithmic design, we present a class containing these functions and closed under the main network calculus operations (min, max, +, −, convolution, subadditive closure, deconvolution): the piecewise affine functions which are ultimately pseudo-periodic. They can be finitely described, which enables us to propose some algorithms for each of the network calculus operations. We finally analyze their computational complexity.

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.     

Calculus Students' Use and Interpretation of Variables: Algebraic vs. Arithmetic Thinking

Abstract

The ability to use and interpret algebraic variables as generalized numbers and changing quantities is fundamental to the learning of calculus. This study considers the use of variables in these advanced ways as a component of algebraic thinking. College introductory calculus students' (n = 174) written responses to algebra problems requiring the use and interpretation of variables as changing quantities were examined for evidence of algebraic and arithmetic thinking. A framework was developed to describe and categorize examples of algebraic, transitional, and arithmetic thinking reflected in these students' uses of variables. The extent to which students' responses showed evidence of algebraic or arithmetic thinking was quantified and related to their course grades. Only one third of the responses of these entering calculus students were identified as representative of algebraic thinking. This study extends previous research by showing that evidence of algebraic thinking in students' work was positively related to successful performance in calculus.     

An Overview of Duration Calculus

TheDurationCalculus(abbreviatedDC)representsalogicalapproachtoformaldesignofreal-timesystems.DCisbasedonintervallOgic,andusestherealnumberstomodeltime,andBoolean-valued(i.e.{0,1}-valued)functionsovertimetomodelstatesandeventsofreaLtimesystems.Thedurationofastateinatimeintervalistheaccumulatedpresencetimeofthestateintheinterval.DCextendsintervallogicwithacalculustospecifyandreasonaboutpropertiesofstatedurations.TheresearchofDCwasintroducedintheProCoSproject(ESPRITBRA3104and7071),whent…     

基于插值细分的逼近细分法

通过在Hassan的四点三重插值细分法中引入一个偏移变量,推导出了一种逼近细分法,从而使三重逼近细分和插值细分统一到一个细分格式.该方法利用细分格式的生成多项式,在理论上分析了提出的细分格式的一致收敛性和Ck连续性;通过对细分格式中参数u取不同的值,可对生成的极限曲线形状进行控制.数值实验结果表明,文中方法是合理有效的.     

算术四则运算智能测试教学软件的设计

采用UML建模和ActionScript技术,为小学数学的加减乘除四则运算设计制作了一种能随机出题、交互解答、智能评测、图音并茂的教学软件。该教学软件克服了传统多媒体教学软件缺乏交互性、随机性的缺点。该软件既可用作小学数学课堂教学,也可放到网页里让学生们自行测试练习。     

曲率连续的有理二次样条插值的一种优化方法

人们通常用有理三次曲线样条来构造整体曲率连续的曲线.提出利用有理二次样条曲线插值整体曲率连续的曲线的一种方法.首先导出了两相邻二次曲线段间曲率连续的拼接条件,然后提出了求解平面上一个闭的点列中每一点处的切线的最优算法.最后给出了闭曲线插值的一些实例以检验方法的有效性.     

An Abstract Machine for a Higher-Order Distributed Process Calculus

This paper presents the formal specification of an abstract machine or the M-calculus, a new distributed process calculus. The M-calculus can be understood as an extension of the Join calculus that realizes an original combination of the following features: programmable localities, higher-order functions and processes, process mobility, and dynamic binding. Our abstract machine covers these different features and presents a modular structure that clearly separates the sequential (functional) evaluation mechanism from the execution core, and the latter from basic marshalling, location and routing mechanisms.     

关于色彩量化的一种算法

描述了一种色彩量化算法。作为对Herkbert的中点切割法的一种改进，本算法考虑到图像色彩的出现频率，以及图象色彩分量在颜色空间的分布情况。     

Sequent calculi and decidability for intuitionistic hybrid logic

In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for IHL and then prove its decidability.