Michael, (01)
I instantly apologize profusely for any mistaken statements I
may have made. (02)
JS>> Michael wants the Process Specification Language (PSL)
>> and the associated reasoning method of situation calculus
>> to be included in the core, (03)
MG> I have never, ever, made that claim!
>
> I've been holding my tongue until now, but you cross the
> line when you impute invalid positions to me personally. (04)
Please don't hold your tongue. If I made any erroneous
assumptions, tell me immediately, and I'll instantly apologize. (05)
If you are not proposing that PSL go into the core, there is
no quarrel whatever between us. My only point was that PSL
and situation calculus be considered one optional module along
with many others based on other approaches, including pi
calculus, Petri nets, etc. (06)
There are other ontologies that have included PSL as their
primary (or only) method for representing processes, and I
mistakenly assumed that you supported that choice for the
ONTAC project. (07)
> My only recommendation (actually more of a plea) is that
> any ontology module should be expressed as a fixed set of
> axioms written in Common Logic, along with the corresponding
> model theory. (08)
On that point, we all agree. (09)
> My objection is with the idea that we should not be mixing
> different logical languages with different model theories within
> the library. This simply compounds the problem of determining
> the relationship between different modules. (010)
The model theory for Common Logic is inherited by all consistent
theories expressed in any CL dialect. And the easiest way to
demonstrate consistency is to write your axioms with at least
one example in mind. (011)
If you take two consistent, but independently written modules,
then proving that they are mutually consistent can be undecidable.
But again, most projects that need a particular module already
have an example in mind. If they adopt a policy of testing each
module against the examples before adopting it, then they can be
sure that their conjunction is consistent. (012)
> How do we know that it is inconsistent if you do not tell us what
> the Common Logic axioms are? (013)
I believe that I can describe the conflict without writing down
any formal axioms. Following is an informal summary of how
to model PSL by means of Petri nets and to model Petri nets
by means of pi calculus. That means that it is, in principle,
possible for all of these theories to co-exist, but only
within a larger framework that takes pi calculus as primary. (014)
The big conflict with PSL is one that I objected to years ago:
the definition of processes in terms of time in a way that
assumes (explicitly or implicitly) a global clock. That may be
useful for some projects, but it creates conflicts with systems
in which (a) there is no clock, (b) there may be local clocks,
but no global clock, (c) causal dependencies among events are
critical, but the exact timing is irrelevant, unpredictable,
or impossible to measure, and (d) messages are passed along
an asynchronous network in which widely separated nodes have
no way (or no convenient way) to synchronize their clocks. (015)
The reason why I prefer Petri nets is that they focus on causal
connections (input and output arcs) rather than timing. Pi
calculus takes the next step beyond Petri nets of allowing the
topology of the networks to change dynamically. (016)
Modeling Petri nets in terms of pi calculus is trivial: just
avoid creating or destroying any nodes in the net. To convert
a Petri net to a PSL model, do the following: (017)
1. Define a small net that represents a clock. It only takes
one transition (called Tick) and two places, one of which
is called Counter. (See Ch. 4 of my KR book, where I do
that). (018)
2. For any given Petri net, add an extra input arc and output
arc for every transition, which reads the clock (i.e.,
inputs a message about the time) before it fires, and
generates a message that states when it fired. (019)
3. A model would consist of a set of copies of the net at each
time stamp. The axioms would consist of CL statements that
specify the firing rules that derive each copy from the
previous copy. (020)
This makes the network much more complicated, but it enables
all processes to fit into the PSL framework with a global time.
The reverse process of going from PSL to a Petri net is more
complex, but I don't think it would be more than a messy
exercise. (021)
John (022)
_________________________________________________________________
Message Archives: http://colab.cim3.net/forum/ontac-forum/
To Post: mailto:ontac-forum@xxxxxxxxxxxxxx
Subscribe/Unsubscribe/Config:
http://colab.cim3.net/mailman/listinfo/ontac-forum/
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
Community Wiki:
http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG (023)
|