Methods for synthesizing concurrent programs from temporal logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson and Clarke and by Manna and Wo...
详细信息
Methods for synthesizing concurrent programs from temporal logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. One only has to formulate a precise problem specification;the synthesis method then mechanically constructs a correct solution. A serious drawback of these methods in practice, however, is that they suffer from the state explosion problem. To synthesize a concurrent system consisting of K sequential processes, each having N states in its local transition diagram, requires construction of the global product-machine having about N-K global states in general. This exponential growth in K makes it infeasible to synthesize systems composed of more than 2 or 3 processes. In this article, we show how to synthesize concurrent systems consisting of many (i.e., a finite but arbitrarily large number K of) similar sequential processes. Our approach avoids construction of the global product-machine for K processes;instead, it constructs a two-process product-machine for a single pair of generic sequential processes. The method is uniform in K, providing a simple template that can be instantiated for each process to yield a solution for any fixed K. The method is also illustrated on synchronization problems from the literature.
This paper formalizes a small object-oriented programming notation. The notation features imperative commands where objects can be shared (aliased), and is rich enough to allow subtypes and recursive object types. The...
详细信息
In this article we investigate agent-oriented programming both from a theoretical and a practical view. We propose an abstract agent programming language with a clear and formally defined semantics. The semantics of o...
详细信息
The proceedings contain 30 papers. The special focus in this conference is on Computer Science logic. The topics include: Call-by-value games;a specification language based on WS2S;evolution as a computational engine;...
ISBN:
(纸本)3540645705
The proceedings contain 30 papers. The special focus in this conference is on Computer Science logic. The topics include: Call-by-value games;a specification language based on WS2S;evolution as a computational engine;timeless games;from action calculi to linear logic;a sequent calculus for circumscription;linear lower bounds and simulations in frege systems with substitutions;a formulation of linear logic based on dependency-relations;resolution and the weak pigeonhole principle;higher-order matching and tree automata;spectra with only unary function symbols;classical proofs via basic logic;full abstractness for a functional/concurrent language with higher-order value-passing;a duality theory for quantitative semantics;a mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion;equational axioms of test algebra;the logic-automaton connection in practice;existence of reduction hierarchies;a game-theoretic, concurrent and fair model of the typed A-calculus, with full recursion;a conjunctive logical characterization of nondeterministic linear time;on the computational complexity of type 2 functionals;categories with algebraic structure;concurrent constraint programming and non-commutative logic;a hierarchical approach to monadic second-order logic over graphs and the monadic quantifier alternation hierarchy over grids and pictures.
作者：
Matz, OUniv Kiel
Inst Informat & Prakt Math D-24098 Kiel Germany
We isolate a technique for showing that a picture language (i.e. a "two-dimensional language") is not recognizable. Then we prove the non-recognizability of a picture language that is both starfree (i.e., de...
详细信息
ISBN:
(纸本)3540643001
We isolate a technique for showing that a picture language (i.e. a "two-dimensional language") is not recognizable. Then we prove the non-recognizability of a picture language that is both starfree (i.e., definable by means of union, concatenation, and complement) and piecewise testable (i.e., definable by means of allowed subpictures), solving an open question in [GR96]. We also define local, locally testable, and locally threshold testable picture languages and summarize known inclusion results for these classes. The classes of piecewise testable, locally testable, and locally threshold testable picture languages can, as in the word case, be characterized by certain (fragments of) first-order logics.
The paper describes a concurrent logic specification language for developing programs that control multiple robots. This language is based on guarded Horn clauses and specifications are atomically transformed into con...
详细信息
The paper describes a concurrent logic specification language for developing programs that control multiple robots. This language is based on guarded Horn clauses and specifications are atomically transformed into concurrent logic programs, yielding executable specifications. They makes it possible to easily implement complex tasks such as concurrency control, communication and multiagent-type profile, solving for multiple robots. An experiment on program development for multiple manipulators was undertaken to show advantages of the specification language. The resulting observations are twofold. First, specifications are more abstract and natural than conventional procedure-oriented programs. Second the amounts of specifications are very shorter than that of the programs developed by the underlying concurrent logic programs are then compiled into C programs with little overhead the proposed language can be useful as a multiple robot programming language with the efficiency for both program execution and developed.
While non-determinism has long been established as a key concept in logicprogramming, its importance in the context of deductive databases was recognized only recently. This paper provides an overview of recent resul...
While non-determinism has long been established as a key concept in logicprogramming, its importance in the context of deductive databases was recognized only recently. This paper provides an overview of recent results on this topic with the aim of providing an introduction to the theory and practice of non-determinism in deductive databases. In particular we (i) recall the main results linking non-deterministic constructs in database languages to the theory of data complexity and the expressibility hierarchy of query languages;(ii) provide a reasoned introduction to effective programming with non-deterministic constructs;(iii) compare the usage of non-deterministic constructs in languages such as LDL++ to that of traditional logicprogramming languages;(iv) discuss the link between the semantics of logic programs with non-deterministic constructs and the stable-model semantics of logic programs with negation.
Many real problems can be treated as constraint satisfaction problems (CSPs), a type of problem for which efficient tools have been developed. Computing the maximum timing separations between the events of a timing sp...
详细信息
Many real problems can be treated as constraint satisfaction problems (CSPs), a type of problem for which efficient tools have been developed. Computing the maximum timing separations between the events of a timing specification falls into this category. In particular, CLP (BNR) is a constraint logicprogramming language which seems well suited to the problem, allowing to draw from the advantages of both CSPs and logicprogramming. Consistency techniques used for solving general CSPs usually produce approximate answers (partial consistency). However, for some specific timing specifications, that is, systems of strictly linear constraints, systems of either max-only or min-only constraints, and systems where linear and either max or min constraints intermix, we show that global consistency can be achieved using CLP based on Relational Interval Arithmetic.
We consider disjunctive Datalog, a powerful database query language based on disjunctive gic programming. Briefly, disjunctive Datalog is a variant of Datalog where disjunctions may appear in the rule heads;advanced v...
详细信息
We consider disjunctive Datalog, a powerful database query language based on disjunctive gic programming. Briefly, disjunctive Datalog is a variant of Datalog where disjunctions may appear in the rule heads;advanced versions also allow for negation in the bodies, which can be handled according to a semantics for negation in disjunctive logicprogramming. In particular, we investigate three different semantics for disjunctive Datalog: the minimal model semantics, the perfect model semantics, and the stable model semantics. For each of these semantics, the expressive power and complexity are studied. We show that the possibility variants of these semantics express the same set of queries. In fact, they precisely capture the complexity class Sigma(2)(p). Thus, unless the Polynomial Hierarchy collapses, disjunctive Datalog is more expressive than normal logicprogramming with negation. These results are not only of theoretical interest;we demonstrate that problems relevant in practice such as computing the optimal tour value in the Traveling Salesman Problem and eigenvector computations can be handled in disjunctive Datalog, but not Datalog with negation (unless the Polynomial Hierarchy collapses). In addition, we study modularity properties of disjunctive Datalog and investigate syntactic restrictions of the formalisms.
A system with multiple interacting agents (whether artificial or human) is often best analyzed using game-theoretic tools. Unfortunately, while the formal foundations are well-established, standard computational techn...
详细信息
A system with multiple interacting agents (whether artificial or human) is often best analyzed using game-theoretic tools. Unfortunately, while the formal foundations are well-established, standard computational techniques for game-theoretic reasoning are inadequate for dealing with realistic games, This paper describes the Gala system, an implemented system that allows the specification and efficient solution of large imperfect information games. The system contains the first implementation of a recent algorithm, due to Koller, Megiddo and von Stengel. Experimental results from the system demonstrate that the algorithm is exponentially faster than the standard algorithm in practice, not just in theory. It therefore allows the solution of games that are orders of magnitude larger than were previously possible. The system also provides a new declarative language for compactly and naturally representing games by their rules. As a whole, the Gala system provides the capability for automated game-theoretic analysis of complex real-world situations. (C) 1997 Elsevier Science B.V.
暂无评论