This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.

Bug 3621 - Formal semantics
Summary: Formal semantics
Alias: None
Product: WS-Policy
Classification: Unclassified
Component: Attachment (show other bugs)
Version: FPWD
Hardware: Macintosh All
: P2 normal
Target Milestone: ---
Assignee: Bijan Parsia
QA Contact: Web Services Policy WG QA List
Depends on:
Reported: 2006-08-23 15:43 UTC by Bijan Parsia
Modified: 2006-09-14 16:48 UTC (History)
0 users

See Also:


Description Bijan Parsia 2006-08-23 15:43:44 UTC
Title - 
	Formal semantics

Description - 
	Much of the language of the framework specification talks as if WS-Policy is a logic (e.g., reason about, logical construct, etc.) and yet the semantics are specified informally, and in no concentrated place. Furthermore, certain aspects of the semantics seem unspecified (e.g., the precise meaning of exactlyOne; first order exclusive disjunction, that + some sort of close world assumption, etc.).

Justification -  
	Clarity and completeness of a specification are always critical. Formalization does not *always* help clarity, at least for a wide audience, but WS-Policy is simple enough that the semantics should be reasonably accessible to anyone who understands truth tables.

	Secondly, if the semantics are as I believe (roughly propositional logic or a very simple description logic) then we gain access to the wealth of tools and algorithms available for these logics. SAT solvers and DL reasoners are highly optimized and used in all sorts of industrial settings.

	Thirdly, various sorts of analysis become easier if we have a clear semantics. On this page:
are some papers and presentations showing how to discover policy containment, equivalence, disjointness, and incoherence.

	Furthermore, certain behaviors of the operators are specified individually (e.g., commutativity, etc.) that would follow from a normal semantics for the operators (e.g., logical and is commutative, etc.) I think this would simplify the spec.

Target - 

Proposal - 
	Let's consider normal form only for the moment.

	I will do it only propositionally at the moment.

	Policy assertions correspond to propositional variables, aka, atomic sentences. There are an infinite number of them.

		<all>P1...Pj</all> is true just in case for i = 1 to j, Pi is true.
		<exactlyOne>A1...Ak</exactlyOne> is true just in case for some i=1 to k, Ai is true and for an m != i, Am is false.

	(Now, when we introduce a policy subject, the propositional letters become one place predicates, but that is easily handled.)

	Clearly this isn't a lot of text, though there are additional details. I just wanted to give a flavor.

	For example, it's easy to show that <all> is communtative, and associative (the truth conditions are independent of order or grouping)
Comment 1 Bijan Parsia 2006-08-30 17:18:36 UTC
Start of thread on this issue:
Comment 2 Bijan Parsia 2006-09-14 16:48:39 UTC
See F2F minutes around: