اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدOn Finite Bases for Weak Semantics: Failures versus Impossible Futures
56
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We provide a finite basis for the (in)equational theory of the process algebra BCCS modulo the weak failures preorder and equivalence. We also give positive and negative results regarding the axiomatizability of BCCS modulo weak impossible futures semantics.
قيم البحث
اقرأ أيضاً
CSP-Agda is a library, which formalises the process algebra CSP in the interactive theorem prover Agda using coinductive data types. In CSP-Agda, CSP processes are in monadic form, which sup- ports a modular development of processes. In this paper, w
e implement two main models of CSP, trace and stable failures semantics, in CSP-Agda, and define the corresponding refinement and equal- ity relations. Because of the monadic setting, some adjustments need to be made. As an example, we prove commutativity of the external choice operator w.r.t. the trace semantics in CSP-Agda, and that refinement w.r.t. stable failures semantics is a partial order. All proofs and definitions have been type checked in Agda. Further proofs of algebraic laws will be available in the CSP-Agda repository.
We consider approaches for causal semantics of Petri nets, explicitly representing dependencies between transition occurrences. For one-safe nets or condition/event-systems, the notion of process as defined by Carl Adam Petri provides a notion of a r
un of a system where causal dependencies are reflected in terms of a partial order. A well-known problem is how to generalise this notion for nets where places may carry several tokens. Goltz and Reisig have defined such a generalisation by distinguishing tokens according to their causal history. However, this so-called individual token interpretation is often considered too detailed. A number of approaches have tackled the problem of defining a more abstract notion of process, thereby obtaining a so-called collective token interpretation. Here we give a short overview on these attempts and then identify a subclass of Petri nets, called structural conflict nets, where the interplay between conflict and concurrency due to token multiplicity does not occur. For this subclass, we define abstract processes as equivalence classes of Goltz-Reisig processes. We justify this approach by showing that we obtain exactly one maximal abstract process if and only if the underlying net is conflict-free with respect to a canonical notion of conflict.
The preferential conditional logic PCL, introduced by Burgess, and its extensions are studied. First, a natural semantics based on neighbourhood models, which generalise Lewis sphere models for counterfactual logics, is proposed. Soundness and comple
teness of PCL and its extensions with respect to this class of models are proved directly. Labelled sequent calculi for all logics of the family are then introduced. The calculi are modular and have standard proof-theoretical properties, the most important of which is admissibility of cut, that entails a syntactic proof of completeness of the calculi. By adopting a general strategy, root-first proof search terminates, thereby providing a decision procedure for PCL and its extensions. Finally, the semantic completeness of the calculi is established: from a finite branch in a failed proof attempt it is possible to extract a finite countermodel of the root sequent. The latter result gives a constructive proof of the finite model property of all the logics considered.
Semantic parsing, as an important approach to question answering over knowledge bases (KBQA), transforms a question into the complete query graph for further generating the correct logical query. Existing semantic parsing approaches mainly focus on r
elations matching with paying less attention to the underlying internal structure of questions (e.g., the dependencies and relations between all entities in a question) to select the query graph. In this paper, we present a relational graph convolutional network (RGCN)-based model gRGCN for semantic parsing in KBQA. gRGCN extracts the global semantics of questions and their corresponding query graphs, including structure semantics via RGCN and relational semantics (label representation of relations between entities) via a hierarchical relation attention mechanism. Experiments evaluated on benchmarks show that our model outperforms off-the-shelf models.
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the
first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
