اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدMeta SOS - A Maude Based SOS Meta-Theory Framework
94
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Meta SOS is a software framework designed to integrate the results from the meta-theory of structural operational semantics (SOS). These results include deriving semantic properties of language constructs just by syntactically analyzing their rule-based definition, as well as automatically deriving sound and ground-complete axiomatizations for languages, when considering a notion of behavioural equivalence. This paper describes the Meta SOS framework by blending aspects from the meta-theory of SOS, details on their implementation in Maude, and running examples.
قيم البحث
اقرأ أيضاً
There exists a rich literature of rule formats guaranteeing different algebraic properties for formalisms with a Structural Operational Semantics. Moreover, there exist a few approaches for automatically deriving axiomatizations characterizing strong
bisimilarity of processes. To our knowledge, this literature has never been extended to the setting with data (e.g. to model storage and memory). We show how the rule formats for algebraic properties can be exploited in a generic manner in the setting with data. Moreover, we introduce a new approach for deriving sound and ground-complete axiom schemata for a notion of bisimilarity with data, called stateless bisimilarity, based on intuitive auxiliary function symbols for handling the store component. We do restrict, however, the axiomatization to the setting where the store component is only given in terms of constants.
Probabilistic transition system specifications (PTSSs) in the $nt mu ftheta / ntmu xtheta$ format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that bisimi
larity is a congruence for all operator defined in such format. Starting from the $nt mu ftheta / ntmu xtheta$ format, we obtain restricted formats that guarantee that three coarser bisimulation equivalences are congruences. We focus on (i) Segalas variant of bisimulation that considers combined transitions, which we call here convex bisimulation; (ii) the bisimulation equivalence resulting from considering Park & Milners bisimulation on the usual stripped probabilistic transition system (translated into a labelled transition system), which we call here probability obliterated bisimulation; and (iii) a probability abstracted bisimulation, which, like bisimulation, preserves the structure of the distributions but instead, it ignores the probability values. In addition, we compare these bisimulation equivalences and provide a logic characterization for each of them.
Structural proof theory is praised for being a symbolic approach to reasoning and proofs, in which one can define schemas for reasoning steps and manipulate proofs as a mathematical structure. For this to be possible, proof systems must be designed a
s a set of rules such that proofs using those rules are correct by construction. Therefore, one must consider all ways these rules can interact and prove that they satisfy certain properties which makes them well-behaved. This is called the meta-theory of a proof system. Meta-theory proofs typically involve many cases on structures with lots of symbols. The majority of cases are usually quite similar, and when a proof fails, it might be because of a sub-case on a very specific configuration of rules. Developing these proofs by hand is tedious and error-prone, and their combinatorial nature suggests they could be automated. There are various approaches on how to automate, either partially or completely, meta-theory proofs. In this paper, I will present some techniques that I have been involved in for facilitating meta-theory reasoning.
A popular numerical method to compute SOS (sum of squares of polynomials) decompositions for polynomials is to transform the problem into semi-definite programming (SDP) problems and then solve them by SDP solvers. In this paper, we focus on reducing
the sizes of inputs to SDP solvers to improve the efficiency and reliability of those SDP based methods. Two types of polynomials, convex cover polynomials and split polynomials, are defined. A convex cover polynomial or a split polynomial can be decomposed into several smaller sub-polynomials such that the original polynomial is SOS if and only if the sub-polynomials are all SOS. Thus the original SOS problem can be decomposed equivalently into smaller sub-problems. It is proved that convex cover polynomials are split polynomials and it is quite possible that sparse polynomials with many variables are split polynomials, which can be efficiently detected in practice. Some necessary conditions for polynomials to be SOS are also given, which can help refute quickly those polynomials which have no SOS representations so that SDP solvers are not called in this case. All the new results lead to a new SDP based method to compute SOS decompositions, which improves this kind of methods by passing smaller inputs to SDP solvers in some cases. Experiments show that the number of monomials obtained by our program is often smaller than that by other SDP based software, especially for polynomials with many variables and high degrees. Numerical results on various tests are reported to show the performance of our program.
Based on symmetry consideration, quasi-one-dimensional (1D) objects, relevant to numerous observables or phenomena, can be classified into eight different types. We provide various examples of each 1D type, and discuss their Symmetry Operational Simi
larity (SOS) relationships, which are often permutable. A number of recent experimental observations, including current-induced magnetization in polar or chiral conductors, non-linear Hall effect in polar conductors, spin-polarization of tunneling current to chiral conductors, and ferro-rotational domain imaging with linear gyration are discussed in terms of (permutable) SOS. In addition, based on (permutable) SOS, we predict a large number of new phenomena in low symmetry materials that can be experimentally verified in the future.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
