TALplanner: A temporal logic based forward chaining planner

We present TALplanner, a forward-chaining planner based on the use of domain-dependent search control knowledge represented as formulas in the Temporal Action Logic (TAL). TAL is a narrative based linear metric time logic used for reasoning about action and change in incompletely specified dynamic environments. TAL is used as the formal semantic basis for TALplanner, where a TAL goal narrative with control formulas is input to TALplanner which then generates a TAL narrative that entails the goal and control formulas. The sequential version of TALplanner is presented. The expressivity of plan operators is then extended to deal with an interesting class of resource types. An algorithm for generating concurrent plans, where operators have varying durations and internal state, is also presented. All versions of TALplanner have been implemented. The potential of these techniques is demonstrated by applying TALplanner to a number of standard planning benchmarks in the literature. This revised version was published online in June 2006 with corrections to the Cover Date.     

Decidable fragments of many-sorted logic

Many natural specifications use types. We investigate the decidability of fragments of many-sorted first-order logic. We identified some decidable fragments and illustrated their usefulness by formalizing specifications considered in the literature. Often the intended interpretations of specifications are finite. We prove that the formulas in these fragments are valid iff they are valid over the finite structures. We extend these results to logics that allow a restricted form of transitive closure.     

On the existence of translations of structured specifications

We provide a set of sufficient conditions for the existence of translations of structured specifications across specification formalisms. The most basic condition is the existence of a translation between the logical systems underlying the specification formalisms, which corresponds to the unstructured situation. Our approach is based upon institution theory and especially upon a recent abstract approach to structured specifications in which both the underlying logics and the structuring systems are treated fully abstractly. Hence our result is applicable to a wide range of actual specification formalisms that may employ different logics as well as different structuring systems, and is very relevant within the context of the fastly developing heterogeneous specification paradigm.     

事件本体中的动作推理研究

事件是随时间变化而变化的具体事实,事件是由动作、时间及其它要素组成,动作是事件定义中的主要构成部分.在面向事件的知识库系统中,关于动作的推理研究一直是重要的研究课题之一.现有的动作推理形式化系统旨在描述和推理现实世界中状态的变化,忽略了时间要素对推理过程的影响.针对这种不足,本文在描述逻辑的基础上扩充了一个Action-TBox和一个Action-ABox,并将事件本体中的动作要素和时间要素相结合,形式化定义了动作的一个三元组表示方式以及多种时间构造算子,用以刻画组合动作的发生过程,在此基础上研究了事件本体中关于动作的几种推理服务.     

Inductive situation calculus

Temporal reasoning has always been a major test case for knowledge representation formalisms. In this paper, we develop an inductive variant of the situation calculus in ID-logic, classical logic extended with inductive definitions. This logic has been proposed recently and is an extension of classical logic. It allows for a uniform representation of various forms of definitions, including monotone inductive definitions and non-monotone forms of inductive definitions such as iterated induction and induction over well-founded posets. We show that the role of such complex forms of definitions is not limited to mathematics but extends to commonsense knowledge representation. In the ID-logic axiomatization of the situation calculus, fluents and causality predicates are defined by simultaneous induction on the well-founded poset of situations. The inductive approach allows us to solve the ramification problem for the situation calculus in a uniform and modular way. Our solution is among the most general solutions for the ramification problem in the situation calculus. Using previously developed modularity techniques, we show that the basic variant of the inductive situation calculus without ramification rules is equivalent to Reiter-style situation calculus.     

An approach to efficient planning with numerical fluents and multi-criteria plan quality

Dealing with numerical information is practically important in many real-world planning domains where the executability of an action can depend on certain numerical conditions, and the action effects can consume or renew some critical continuous resources, which in pddl can be represented by numerical fluents. When a planning problem involves numerical fluents, the quality of the solutions can be expressed by an objective function that can take different plan quality criteria into account.We propose an incremental approach to automated planning with numerical fluents and multi-criteria objective functions for pddl numerical planning problems. The techniques in this paper significantly extend the framework of planning with action graphs and local search implemented in the lpg planner. We define the numerical action graph (NA-graph) representation for numerical plans and we propose some new local search techniques using this representation, including a heuristic search neighborhood for NA-graphs, a heuristic evaluation function based on relaxed numerical plans, and an incremental method for plan quality optimization based on particular search restarts. Moreover, we analyze our approach through an extensive experimental study aimed at evaluating the importance of some specific techniques for the performance of the approach, and at analyzing its effectiveness in terms of fast computation of a valid plan and quality of the best plan that can be generated within a given CPU-time limit. Overall, the results show that our planner performs quite well compared to other state-of-the-art planners handling numerical fluents.     

On Action Logic: Equational Theories of Action Algebras

Pratt (1991, Proceedings of JELIA’90, Volume 478, pp.97–120) defines action algebras as Kleene algebras withresiduals and action logic as the equational theory of actionalgebras. In contrast to Kleene algebras, action algebras forma (finitely based) variety. Jipsen (2004, Studia Logica, 76,291–303) proposes a Gentzen-style sequent system for actionlogic but leaves it as an open question if this system admitscut-elimination and if action logic is decidable. We show thatJipsen's system does not admit cut-elimination. We prove thatthe equational theory of *-continuous action algebras and thesimple Horn theory of *-continuous Kleene algebras are not recursivelyenumerable and they possess FMP, but action logic does not possessFMP.     

Distributed synthesis for well-connected architectures

We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly well-connected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.     

On the algebra of structured specifications

We develop module algebra for structured specifications with model oriented denotations. Our work extends the existing theory with specification building operators for non-protecting importation modes and with new algebraic rules (most notably for initial semantics) and upgrades the pushout-style semantics of parameterized modules to capture the (possible) sharing between the body of the parameterized modules and the instances of the parameters. We specify a set of sufficient abstract conditions, smoothly satisfied in the actual situations, and prove the isomorphism between the parallel and the serial instantiation of multiple parameters. Our module algebra development is done at the level of abstract institutions, which means that our results are very general and directly applicable to a wide variety of specification and programming formalisms that are rigorously based upon some logical system.     

Active learning with effective scoring functions for semi-supervised temporal action localization

Temporal Action Localization (TAL) aims to predict both action category and temporal boundary of action instances in untrimmed videos, i.e., start and end time. Existing works usually adopt fully-supervised solutions, however, one of the practical bottlenecks in these solutions is the large amount of labeled training data required. To reduce expensive human label cost, this paper focuses on a rarely investigated yet practical task named semi-supervised TAL and proposes an effective active learning method, named AL-STAL. We leverage four steps for actively selecting video samples with high informativeness and training the localization model, named Train, Query, Annotate, Append. Two scoring functions that consider the uncertainty of localization model are equipped in AL-STAL, thus facilitating the video sample ranking and selection. One takes entropy of predicted label distribution as measure of uncertainty, named Temporal Proposal Entropy (TPE). And the other introduces a new metric based on mutual information between adjacent action proposals, named Temporal Context Inconsistency (TCI). To validate the effectiveness of proposed method, we conduct extensive experiments on three benchmark datasets THUMOS’14, ActivityNet 1.3 and ActivityNet 1.2. Experiment results show that AL-STAL outperforms the existing competitors and achieves satisfying performance compared with fully-supervised learning.     

Formal Verification of Activity-Based Specification of Protocols

In this paper, we describe a method to formally verify activity-based specifications such as EBSDL. Starting from EBSDL-like specifications that specify engineering activities in terms of input and output behaviors, we derive programs in an asynchronous language CSP-R. CSP-R programs are then verified by the Maxpar method by composing them with the programs abstracting their environment. EBSDL-like specification and its verification using our method, is illustrated through the example of a fragment of LAPD protocol. The derivation of programs from the specification of activities of the underlying protocols through EBSDL-like specifications provides an important useful tool for formal verification of real-time protocols. We shall also discuss a translation of EBSDL-like specifications to synchronous languages such as Esterel. In the method proposed, it is possible for the user to choose asynchronous or synchronous formalisms depending upon the requirements of verification vis-a-vis logical specification.     

Invariant-driven specifications in Maude

This work presents a general mechanism for executing specifications that comply with given invariants, which may be expressed in different formalisms and logics. We exploit Maude’s reflective capabilities and its properties as a general semantic framework to provide a generic strategy that allows us to execute Maude specifications taking into account user-defined invariants. The strategy is parameterized by the invariants and by the logic in which such invariants are expressed. We experiment with different logics, providing examples for propositional logic, (finite future time) linear temporal logic and metric temporal logic.     

一种检测TAL-freeness的代数方法

时间动作锁(Ti me-Action-Lock,TAL)指的是实时系统处于一种时间无法继续同时又没有任何动作能够发生的状态.Behzad和Kozo在时间自动机的几何学基础上提出了一种针对TAL-freeness的检测方法.但该方法要求必须将需要检测的模型转化为一种逻辑语言Rational Presburger Sentences后才能进行检测,因此使得验证过程比较繁琐.文中提出了一种检测TAL-freeness的代数方法,能够直接对系统模型进行直接验证,并且能够定位死锁原因.针对该方法,文中还给出了相应算法并提供了正确性证明与性能分析.     

Learning to Take Actions

We formalize a model for supervised learning of action strategies in dynamic stochastic domains and show that PAC-learning results on Occam algorithms hold in this model as well. We then identify a class of rule-based action strategies for which polynomial time learning is possible. The representation of strategies is a generalization of decision lists; strategies include rules with existentially quantified conditions, simple recursive predicates, and small internal state, but are syntactically restricted. We also study the learnability of hierarchically composed strategies where a subroutine already acquired can be used as a basic action in a higher level strategy. We prove some positive results in this setting, but also show that in some cases the hierarchical learning problem is computationally hard.     

Certifying Compilation and Run-Time Code Generation

A certifying compiler takes a source language program and produces object code, as well as a certificate that can be used to verify that the object code satisfies desirable properties, such as type safety and memory safety. Certifying compilation helps to increase both compiler robustness and program safety. Compiler robustness is improved since some compiler errors can be caught by checking the object code against the certificate immediately after compilation. Program safety is improved because the object code and certificate alone are sufficient to establish safety: even if the object code and certificate are produced on an unknown machine by an unknown compiler and sent over an untrusted network, safe execution is guaranteed as long as the code and certificate pass the verifier.Existing work in certifying compilation has addressed statically generated code. In this paper, we extend this to code generated at run time. Our goal is to combine certifying compilation with run-time code generation to produce programs that are both fast and verifiably safe. To achieve this goal, we present two new languages with explicit run-time code generation constructs: Cyclone, a type safe dialect of C, and TAL/T, a type safe assembly language. We have designed and implemented a system that translates a safe C program into Cyclone, which is then compiled to TAL/T, and finally assembled into executable object code. This paper focuses on our overall approach and the front end of our system; details about TAL/T will appear in a subsequent paper.     

Typing termination in a higher-order concurrent imperative language

We propose means to predict termination in a higher-order imperative and concurrent language à la ML. We follow and adapt the classical method for proving termination in typed formalisms, namely the realizability technique. There is a specific difficulty with higher-order state, which is that one cannot define a realizability interpretation simply by induction on types, because applying a function may have side-effects at types not smaller than the type of the function. Moreover, such higher-order side-effects may give rise to computations that diverge without resorting to explicit recursion. We overcome these difficulties by introducing a type and effect system for our language that enforces a stratification of the memory. The stratification prevents the circularities in the memory that may cause divergence, and allows us to define a realizability interpretation of the types and effects, which we then use to establish that typable sequential programs in our system are guaranteed to terminate, unless they use explicit recursion in a divergent way. We actually prove a more general fairness property, that is, any typable thread yields the scheduler after some finite computation. Our realizability interpretation also copes with dynamic thread creation.     

Structuring Optimizing Transformations and Proving Them Sound

A compiler optimization is sound if the optimized program that it produces is semantically equivalent to the input program. The proofs of semantic equivalence are usually tedious. To reduce the efforts required, we identify a set of common transformation primitives that can be composed sequentially to obtain specifications of optimizing transformations. We also identify the conditions under which the transformation primitives preserve semantics and prove their sufficiency. Consequently, proving the soundness of an optimization reduces to showing that the soundness conditions of the underlying transformation primitives are satisfied.The program analysis required for optimization is defined over the input program whereas the soundness conditions of a transformation primitive need to be shown on the version of the program on which it is applied. We express both in a temporal logic. We also develop a logic called temporal transformation logic to correlate temporal properties over a program (seen as a Kripke structure) and its transformation.An interesting possibility created by this approach is a novel scheme for validating optimizer implementations. An optimizer can be instrumented to generate a trace of its transformations in terms of the transformation primitives. Conformance of the trace with the optimizer can be checked through simulation. If soundness conditions of the underlying primitives are satisfied by the trace then it preserves semantics.     

COMPLEXITY RESULTS FOR SAS+ PLANNING

We have previously reported a number of tractable planning problems defined in the SAS⁺ formalism. This article complements these results by providing a complete map over the complexity of SAS⁺ planning under all combinations of the previously considered restrictions. We analyze the complexity of both finding a minimal plan and finding any plan. In contrast to other complexity surveys of planning, we study not only the complexity of the decision problems but also the complexity of the generation problems. We prove that the SAS⁺-PUS problem is the maximal tractable problem under the restrictions we have considered if we want to generate minimal plans. If we are satisfied with any plan, then we can generalize further to the SAS⁺-US problem, which we prove to be the maximal tractable problem in this case.