The aim of this article is developing a formal system suitable for reasoning about the distance between propositional formulas. We introduce and study a formal language which is the extension of the classical propositional language obtained by adding new binary operators D≤s and D≥s , s ∈ Range, where Range is a fixed finite set. In our language it is allowed to make formulas of the form D≤s (α ; β ) with the intended meaning ’distance between formulas α and β is less than or equal to s ’. The semantics of the proposed language consists of possible worlds with a distance function defined between sets of worlds.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this work we consider modeling of workflow systems with Petri nets. To increase flexibility and give tools for workflow models re-engineering we extend the formalism of workflow nets by considering systems of interacting nets. Then we study soundness – the main correctness property of workflow processes – and show, that for a special class of structured workflow system soundness can be proved in compositional way.
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this paper we consider adaptive workflow nets, a class of nested nets that allows more comfort and expressive power for modeling adaptability and exception handling in workflow nets. We define two important behavioural properties of adaptive workflow nets: soundness and circumspectness. Soundness means that a proper final marking (state) can be reached from any marking which is reachable from the initial marking, and no garbage will be left. Circumspectness means that the upper layer is always ready to handle any exception that can happen in a lower layer. We define a finite state abstraction for adaptive workflow nets and show that soundness and circumspectness can be verified on this abstraction.
4
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
For designing and analyzing complex workflow nets the notion of hierarchical decomposition can be essential for keeping the structure of the workflow comprehensible. In this paper we study two classes of nets: hierarchical nets and extended hierarchical nets. The first have a simple hierarchical structure and can be defined in terms of five simple refinement rules. We show that for arbitrary nets it can be easily verified if they can be constructed this way, thus confirming their good design and the properties following from it. As we prove, this can be done by performing the refinements in reverse, i.e., by contracting subnets into single nodes. It is shown that the choice of the contracted subnet does not change the final result of the process, and therefore this procedure for checking the hierarchical structure requires no back-tracking. The second class, extended hierarchical nets, is an extension of the first class where two types of extra refinements are introduced that allow to indicate (1) the synchronization between two parallel running subworkflows or (2) the transfer of a thread from one subworkflow to another one. These refinements come with natural and necessary preconditions that ensure that result is still a sound workflow net. In case (1) where we want to synchronize two actions in two subworkflows, we should convince ourselves that the subworkflows represent parallel threads which always execute together, otherwise a deadlock could easily arise. Dually, in case (2), if after the moment that a choice was made between two subworkflows we at a later point in the workflow want to allow a transfer between them, this can be done safely provided that we did not enter any thread fork in the meantime. We show that the class of extended hierarchical nets, which is defined by adding these two additional types of refinement, is a proper superset of the hierarchical nets, but still all such nets exhibit the correctness property of *-soundness. We do this by showing that the class is a proper subset of the AND-OR nets which were in earlier work shown to have this property.
5
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Classical workflow nets (WF-nets for short) are an important subclass of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property of workflow systems and guarantees that these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable for WF-nets and can be polynomially solvable for free-choice WF-nets. This paper proves that the soundness problem is PSPACE-hard for WF-nets. Furthermore, it is proven that the soundness problem is PSPACE-complete for bounded WF-nets. Based on the above conclusion, it is derived that the soundness problem is also PSPACE-complete for bounded WF-nets with reset or inhibitor arcs (ReWF-nets and InWF-nets for short, resp.). ReWF- and InWF-nets are two extensions to WF-nets and their soundness problems were proven by Aalst et al. to be undecidable. Additionally, we prove that the soundness problem is co-NP-hard for asymmetric-choice WF-nets that are a larger class and can model more cases of interaction and resource allocation than free-choice ones.
The aim of the article is to present ways of appellate courts to assess judgments of lower courts. The source of the analyzed linguistic material are judgments of the Appellate Court and District Court in Bialystok. The overriding criterion for this assessment is the value referred to as “fairness”. The considerations concern the ways of expressing the assessment of the utterance in such a species-specific type of text, which is the justification of the court’s judgment. My goal is to initially identify lexical exponents of equity in a few selected texts and their typological ordering.
7
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this paper we consider workflow nets as dynamical systems governed by ordinary difference equations described by a particular class of Petri nets. Workflow nets are a formal model of business processes. Well-formed business processes correspond to sound workflow nets. Even if it seems necessary to require the soundness of workflow nets, there exist business processes with conditional behavior that will not necessarily satisfy the soundness property. In this sense, we propose an analytical method for showing that a workflow net satisfies the classical soundness property using a Petri net. To present our statement, we use Lyapunov stability theory to tackle the classical soundness verification problem for a class of dynamical systems described by Petri nets. This class of Petri nets allows a dynamical model representation that can be expressed in terms of difference equations. As a result, by applying Lyapunov theory, the classical soundness property for workflow nets is solved proving that the Petri net representation is stable. We show that a finite and non-blocking workflow net satisfies the sound property if and only if its corresponding PN is stable, i.e., given the incidence matrix A of the corresponding PN, there exists a Φ strictly positive m vector such that AΦ ≤ 0. The key contribution of the paper is the analytical method itself that satisfies part of the definition of the classical soundness requirements. The method is designed for practical applications, guarantees that anomalies can be detected without domain knowledge, and can be easily implemented into existing commercial systems that do not support the verification of workflows. The validity of the proposed method is successfully demonstrated by application examples.
In this paper we consider workflow nets as dynamical systems governed by ordinary difference equations described by a particular class of Petri nets. Workflow nets are a formal model of business processes. Well-formed business processes correspond to sound workflow nets. Even if it seems necessary to require the soundness of workflow nets, there exist business processes with conditional behavior that will not necessarily satisfy the soundness property. In this sense, we propose an analytical method for showing that a workflow net satisfies the classical soundness property using a Petri net. To present our statement, we use Lyapunov stability theory to tackle the classical soundness verification problem for a class of dynamical systems described by Petri nets. This class of Petri nets allows a dynamical model representation that can be expressed in terms of difference equations. As a result, by applying Lyapunov theory, the classical soundness property for workflow nets is solved proving that the Petri net representation is stable. We show that a finite and non-blocking workflow net satisfies the sound property if and only if its corresponding PN is stable, i.e., given the incidence matrix A of the corresponding PN, there exists a Φ strictly positive m vector such that AΦ ≤ 0. The key contribution of the paper is the analytical method itself that satisfies part of the definition of the classical soundness requirements. The method is designed for practical applications, guarantees that anomalies can be detected without domain knowledge, and can be easily implemented into existing commercial systems that do not support the verification of workflows. The validity of the proposed method is successfully demonstrated by application examples.
In this paper, we shall show that the following translation \(I^M\) from the propositional fragment \(\bf L_1\) of Leśniewski's ontology to modal logic \(\bf KTB\) is sound: for any formula \(\phi\) and \(\psi\) of \(\bf L_1\), it is defined as (M1) \(I^M(\phi \vee \psi) = I^M(\phi) \vee I^M(\psi)\), (M2) \(I^M(\neg \phi) = \neg I^M(\phi)\), (M3) \(I^M(\epsilon ab) = \Diamond p_a \supset p_a . \wedge . \Box p_a \supset \Box p_b .\wedge . \Diamond p_b \supset p_a\), where \(p_a\) and \(p_b\) are propositional variables corresponding to the name variables \(a\) and \(b\), respectively. In the last, we shall give some comments including some open problems and my conjectures.
We introduce a first order extension of GL, called ML3, and develop its proof theory via a proxy cut-free sequent calculus GLTS. We prove the highly nontrivial result that cut is a derived rule in GLTS, a result that is unavailable in other known first-order extensions of GL. This leads to proofs of weak reflection and the related conservation result for ML3, as well as proofs for Craig’s interpolation theorem for GLTS. Turning to semantics we prove that ML3 is sound with respect to arithmetical interpretations and that it is also sound and complete with respect to converse well-founded and transitive finite Kripke models. This leads us to expect that a Solovay-like proof of arithmetical completeness of ML3 is possible.
11
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to intersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest—soundness, completeness, and type safety—we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems—one for call-by-value and one for call-by-name evaluation—which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe.
12
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
This paper discusses issues related to incomplete information databases and considers a logical framework for rule generation. In our approach, a rule is an implication satisfying specified constraints. The term incomplete information databases covers many types of inexact data, such as non-deterministic information, data with missing values, incomplete information or interval valued data. In the paper, we start by defining certain and possible rules based on non-deterministic information. We use their mathematical properties to solve computational problems related to rule generation. Then, we reconsider the NIS-Apriori algorithm which generates a given implication if and only if it is either a certain rule or a possible rule satisfying the constraints. In this sense, NIS-Apriori is logically sound and complete. In this paper, we pay a special attention to soundness and completeness of the considered algorithmic framework, which is not necessarily obvious when switching from exact to inexact data sets. Moreover, we analyze different types of non-deterministic information corresponding to different types of the underlying attributes, i.e., value sets for qualitative attributes and intervals for quantitative attributes, and we discuss various approaches to construction of descriptors related to particular attributes within the rules' premises. An improved implementation of NIS-Apriori and some demonstrations of an experimental application of our approach to data sets taken from the UCI machine learning repository are also presented. Last but not least, we show simplified proofs of some of our theoretical results.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.