Sequential Function Chart (SFC) is a graphical programming language defined in IEC 61131-3 as a standard programming language for Programable logic Controllers (PLCs). It provides an excellent method for formal specif...
详细信息
ISBN:
(纸本)0889865027
Sequential Function Chart (SFC) is a graphical programming language defined in IEC 61131-3 as a standard programming language for Programable logic Controllers (PLCs). It provides an excellent method for formal specification of discrete events systems. In this paper we describe a method to implement SFCs using Field Programmable Gate Arrays (FPGAs). the method is based on converting the SFC to a Very High Speed Integrated Circuit (VHSIC) Hardware Description Language (VHDL) which is a standard language used to configure FPGAs. the algorithm is successfully employed on an experimental platform using Xilinx Spartan-3 FPGA. Implementing SFCs on FPGAs satisfy the requirements of downsizing, hiding information, reducing costs, while adding high speed capabilities.
We propose a new parameter for the complexity of finite directed graphs which measures to what extent the cycles of the graph are intertwined. this measure, called entanglement, is defined by way of a game that is som...
详细信息
ISBN:
(纸本)3540252363
We propose a new parameter for the complexity of finite directed graphs which measures to what extent the cycles of the graph are intertwined. this measure, called entanglement, is defined by way of a game that is somewhat similar in spirit to the robber and cops games used to describe tree width, directed tree width, and hypertree width. Nevertheless, on many classes of graphs, there are significant differences between entanglement and the various incarnations of tree width. Entanglement is intimately connected to the computational and descriptive complexity of the modal μ-calculus. On the one hand, the number of fixed point variables needed to describe a finite graph up to bisimulation is captured by its entanglement. this plays a crucial role in the proof that the variable hierarchy of the μ-calculus is strict. In addition to this, we prove that parity games of bounded entanglement can be solved in polynomial time. Specifically, we establish that the complexity of solving a parity game can be parametrised in terms of the minimal entanglement of a subgame induced by a winning strategy.
this paper focuses on policy languages for (role-based) access control [14, 32], especially in their modern incarnations in the form of trust-management systems [9] and usage control [30, 31]. Any (declarative) approa...
详细信息
ISBN:
(纸本)1595930906
this paper focuses on policy languages for (role-based) access control [14, 32], especially in their modern incarnations in the form of trust-management systems [9] and usage control [30, 31]. Any (declarative) approach to access control and trust management has to address the following issues: Explicit denial, inheritance, and overriding, and History-sensitive access control Our main contribution is a policy algebra, in the timed concurrent constraint programming paradigm, that uses a form of default constraint programming to address the first issue, and reactive computing to address the second issue. the policy algebra is declarative - programs can be viewed as imposing temporal constraints on the evolution of the system - and supports equational reasoning. the validity of equations is established by coinductive proofs based on an operational semantics. the design of the policy algebra supports reasoning about policies by a systematic combination of constraint reasoning and model checking techniques based on linear time temporal-logic. Our framework permits us to perform security analysis with dynamic state-dependent restrictions. Copyright 2005 ACM.
We propose a model to manage the distributed computation of answer sets within a general framework. this design incorporates a variety of software and hardware architectures and allows its easy use with a diverse cadr...
详细信息
ISBN:
(纸本)3540285385
We propose a model to manage the distributed computation of answer sets within a general framework. this design incorporates a variety of software and hardware architectures and allows its easy use with a diverse cadre of computational elements. Starting from a generic algorithmic scheme, we develop a platform for distributed answer set computation, describe its current state of implementation, and give some experimental results.
Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. basic superposition, a calculus highly ...
详细信息
ISBN:
(纸本)3540252363
Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. basic superposition, a calculus highly optimized for theorem proving with equality. However, even such an advanced calculus does not restrict inferences enough to obtain decision procedures for complex logics, such as SHIQ. In this paper, we present a new decomposition inference rule, which can be combined with any resolution-based calculus compatible withthe standard notion of redundancy. We combine decomposition with basic superposition to obtain three new decision procedures: (i) for the description logic SHIQ, (ii) for the description logic ALCHIQb, and (iii) for answering conjunctive queries over SHIQ knowledge bases. the first two procedures are worst-case optimal and, based on the vast experience in building efficient theorem provers, we expect them to be suitable for practical usage.
We give a monadic semantics in the category of FM-cpos to a higher-order CBV language with recursion and dynamically allocated mutable references that may store both ground data and the addresses of other references, ...
详细信息
ISBN:
(数字)9783540320142
ISBN:
(纸本)3540255931
We give a monadic semantics in the category of FM-cpos to a higher-order CBV language with recursion and dynamically allocated mutable references that may store both ground data and the addresses of other references, but not functions. this model is adequate, though far from fully abstract. We then develop a relational reasoning principle over the denotational model, and show how it may be used to establish various contextual equivalences involving allocation and encapsulation of store.
alpha Prolog is a logicprogramming language which is well-suited for rapid prototyping of type systems and operational semantics of typed A-calculi and many other languages involving bound names. In alpha Prolog, the...
详细信息
ISBN:
(数字)9783540320142
ISBN:
(纸本)3540255931
alpha Prolog is a logicprogramming language which is well-suited for rapid prototyping of type systems and operational semantics of typed A-calculi and many other languages involving bound names. In alpha Prolog, the nominal unification algorithm of Urban, Pitts and Gabbay is used instead of first-order unification. However, although alpha Prolog can be viewed as Horn-clause logicprogramming in Pitts' nominal logic, proof search using nominal unification is incomplete in nominal logic. Because of nominal logic's equivariance principle, complete proof search would require solving NP-hard equivariant unification problems. Nevertheless, the alpha Prolog programs we studied run correctly without equivariant unification. In this paper, we give several examples of alpha Prolog programs that do not require equivariant unification, develop a test for identifying such programs, and prove the correctness of this test via a proof-theoretic argument.
We show that a minimal dependent type theory based on Sigma-types and equality is degenerated in presence of computational classical logic. By computational classical logic is meant a classical logic derived from a co...
详细信息
ISBN:
(数字)9783540320142
ISBN:
(纸本)3540255931
We show that a minimal dependent type theory based on Sigma-types and equality is degenerated in presence of computational classical logic. By computational classical logic is meant a classical logic derived from a control operator equipped with reduction rules similar to the ones of Felleisen's C or Parigot's mu operators. As a consequence, formalisms such as Martin-Lof's type theory or the (Set-predicative variant of the) Calculus of Inductive Constructions are inconsistent in presence of computational classical logic. Besides, an analysis of the role of the eta-rule for control operators through a set-theoretic model of computational classical logic is given.
Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translation to CNF. Probably the best known example of this is the parity-family. Large instances of such CNF f...
详细信息
ISBN:
(纸本)354027829X
Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translation to CNF. Probably the best known example of this is the parity-family. Large instances of such CNF formulas cannot be solved in reasonable time if no detection of, and extra reasoning with, these clauses is incorporated. that is, in solving these formulas, there is a more or less separate algorithmic device dealing withthe equivalence clauses, called equivalence reasoning, and another dealing withthe remaining clauses. In this paper we propose a way to align these two reasoning devices by introducing parameters for which we establish optimal values over a variety of existing benchmarks. We obtain a truly convincing speed-up in solving such formulas with respect to the best solving methods existing so far.
Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logicprogramming and...
详细信息
ISBN:
(纸本)3540255966
Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logicprogramming and term rewriting techniques that provide similar advantages to, but remain simpler than, higher-order logicprogramming or term rewriting systems. Previous work on nominal rewriting and logicprogramming has relied on nominal unification, that is, unification up to equality in nominal logic. However, because of nominal logic's equivariance property, these applications require a stronger form of unification, which we call equivariant unification. Unfortunately, equivariant unification and matching are NP-hard decision problems. this paper presents an algorithm for equivariant unification that produces a complete set of finitely many solutions, as well as NP decision procedure and a version that enumerates solutions one at a time. In addition, we present a polynomial time algorithm for swapping-free equivariant matching, that is, for matching problems in which the swapping operation does not appear.
暂无评论