This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax boolean OR E), the E;Ax-variants of a term t are understood as the set of all pairs consi...
详细信息
ISBN:
(纸本)9783939897309
This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax boolean OR E), the E;Ax-variants of a term t are understood as the set of all pairs consisting of a substitution sigma and the E;Ax-canonical form of t sigma. The equational theory (Ax boolean OR E) has the finite variant property iff there is a finite set of most general variants. We have added support in Maude 2.6 for: (i) order-sorted unification modulo associativity, commutativity and identity, (ii) variant generation, (iii) order-sorted unification modulo finite variant theories, and (iv) narrowing-based symbolic reachability modulo finite variant theories. We also explain how these features have a number of interesting applications in areas such as unification theory, cryptographic protocol verification, business processes, and proofs of termination, confluence and coherence.
This paper investigates belief revision where the underlying logic is that governing Horn clauses. It proves to be the case that classical (AGM) belief revision doesn't immediately generalise to the Horn case. In ...
详细信息
ISBN:
(纸本)9781577355120
This paper investigates belief revision where the underlying logic is that governing Horn clauses. It proves to be the case that classical (AGM) belief revision doesn't immediately generalise to the Horn case. In particular, a standard construction based on a total preorder over possible worlds may violate the accepted (AGM) postulates. Conversely, Horn revision functions in the obvious extension to the AGM approach are not captured by total preorders over possible worlds. We address these difficulties by first restricting the semantic construction to "well behaved" orderings;and second, by augmenting the revision postulates by an additional postulate. This additional postulate is redundant in the AGM approach but not in the Horn case. In a representation result we show that these two approaches coincide. Arguably this work is interesting for several reasons. It extends AGM revision to inferentially-weaker Horn theories;hence it sheds light on the theoretical underpinnings of belief change, as well as generalising the AGM paradigm. Thus, this work is relevant to revision in areas that employ Horn clauses, such as deductive databases andlogicprogramming, as well as areas in which inference is weaker than classical logic, such as in description logic.
Reconfiguration is an important activity for companies selling configurable products or services which have a long life time. However, identification of a set of required changes in a legacy configuration is a hard pr...
详细信息
Reconfiguration is an important activity for companies selling configurable products or services which have a long life time. However, identification of a set of required changes in a legacy configuration is a hard problem, since even small changes in the requirements might imply significant modifications. In this paper we show a solution based on answer set programming, which is a logic-based knowledge representation formalism well suited for a compact description of (re)configuration problems. Its applicability is demonstrated on simple abstractions of several real-world scenarios. The evaluation of our solution on a set of benchmark instances derived from commercial (re)configuration problems shows practical applicability.
The kernel density estimation (KDE)-based image segmentation algorithm has excellent segmentation performance. However, this algorithm is computational intensive. In addition, although this algorithm can tolerant nois...
详细信息
ISBN:
(纸本)9781457712920
The kernel density estimation (KDE)-based image segmentation algorithm has excellent segmentation performance. However, this algorithm is computational intensive. In addition, although this algorithm can tolerant noise in the input images, such as the noise due to snow, rain, or camera shaking, it is sensitive to the noise from the internal computing circuits, such as the noise due to soft errors or PVT (process, voltage, and temperature) variation. Tolerating this kind of noise becomes more and more important as device scaling continues to nanoscale dimensions. Stochastic computing, which uses streams of random bits (stochastic bits streams) to perform computation with conventional digital logic gates, can guarantee reliable computation using unreliable devices. In this paper, we present a stochastic computing implementation of the KDE-based image segmentation algorithm. Our experimental results show that, under the same time constraint, the stochastic implementation is much more tolerant of faults and consumes less hardware and power compared to a conventional (non-stochastic) implementation. Furthermore, compared to a Triple Modular Redundancy (TMR) fault tolerance technique, the stochastic architecture tolerates substantially more soft errors with lower power consumption.
In this paper we will briefly touch distinctive characteristics of the generations known as baby boomers, generation x, generation y, and generation z;and then propose the use of e-portfolio (EP) as a learning and tea...
详细信息
The proceedings contain 7 papers. The topics discussed include: a graphical framework for supporting mass customization;modeling configuration knowledge in heterogeneous product families;(re)configuration using answer...
The proceedings contain 7 papers. The topics discussed include: a graphical framework for supporting mass customization;modeling configuration knowledge in heterogeneous product families;(re)configuration using answer set programming;enumeration of valid partial configurations;incremental prediction of configurator input values based on association rules - a case study;when to use what: structuralization, specialization, instantiation, metaization - some hints for knowledge engineers;and SiMoL - a modeling language for simulation and (re-)configuration.
When defining the semantics of shared-memory concurrent programming languages, one conventionally has to make assumptions about the atomicity of actions such as assignments. Running on physical hardware, these assumpt...
详细信息
ISBN:
(纸本)9783642232169;9783642232176
When defining the semantics of shared-memory concurrent programming languages, one conventionally has to make assumptions about the atomicity of actions such as assignments. Running on physical hardware, these assumptions can fail to hold in practice, which puts in question reasoning about their concurrent execution. We address an observation, due to John Reynolds, that processes proved sound in concurrent separation logic are separated to an extent that these assumptions can be disregarded, so judgements remain sound even if the assumptions on atomicity fail to hold. We make use of a Petri-net based semantics for concurrent separation logic with explicit representations of the key notions of ownership and interference. A new characterization of the separation of processes is given and is shown to be stronger than existing race-freedom results for the logic. Exploiting this, sufficient criteria are then established for an operation of refinement of processes capable of changing the atomicity of assignments.
We define an extension of stit logic that encompasses subjective probabilities representing beliefs about simultaneous choice exertion of other agents. The formalism enables us to express the notion of 'attempt...
详细信息
ISBN:
(纸本)9781577355120
We define an extension of stit logic that encompasses subjective probabilities representing beliefs about simultaneous choice exertion of other agents. The formalism enables us to express the notion of 'attempt' as a choice exertion that maximizes the chance of success with respect to an action effect. The notion of attempt (or effort) is central in philosophical and legal discussions on responsibility and liability.
The proceedings contain 36 papers. The topics discussed include: Causal Nets: a modeling language tailored towards process discovery;on expressive powers of timed logics: comparing boundedness, non-punctuality, and de...
ISBN:
(纸本)9783642232169
The proceedings contain 36 papers. The topics discussed include: Causal Nets: a modeling language tailored towards process discovery;on expressive powers of timed logics: comparing boundedness, non-punctuality, and deterministic freezing;coarse abstractions make Zeno behaviours difficult to detect;a spectrum of behavioral relations over LTSs on Probability Distributions;An Automaton over data words that captures EMSO logic;reachability of multistack pushdown systems with scope-bounded matching relations;tractable reasoning in a fragment of separation logic;controlling reversibility in higher-order pi;a connector algebra for P/T nets interactions;static livelock analysis in CSP;efficient CTL model-checking for pushdown systems;reasoning about threads with bounded lock chains;two variable vs. linear temporal logic in model checking and games;and a compositional framework for controller synthesis.
暂无评论