From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5141 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: categories and formal verification Date: Fri, 11 Sep 2009 18:25:13 -0700 Message-ID: Reply-To: Vaughan Pratt NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1252847298 21274 80.91.229.12 (13 Sep 2009 13:08:18 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 13 Sep 2009 13:08:18 +0000 (UTC) To: categories Original-X-From: categories@mta.ca Sun Sep 13 15:08:11 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1MmooM-0003EF-Se for gsmc-categories@m.gmane.org; Sun, 13 Sep 2009 15:08:11 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1MmoKi-0002bZ-SD for categories-list@mta.ca; Sun, 13 Sep 2009 09:37:32 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5141 Archived-At: David CHEMOUIL wrote: > But, although my colleagues, are pretty convinced by the "constructive" > aspects of CT applied to such matters, they don't see how CT can provide > support in *verifying* things about systems under study (e.g what does CT > approaches bring to check the absence of deadlocks in a concurrent system?). When deadlocks are modeled in the geometric manner of Papadimitriou's "Concurrency Control," one can apply categorical methods as in @InProceedings( Pr91a, Author="Pratt, V.R.", Title="Modeling Concurrency with Geometry", Booktitle="Proc. 18th Ann. ACM Symposium on Principles of Programming Languages", Pages="311-322", Month=Jan, Year=1991) downloadable as http://boole.stanford.edu/pub/cg.pdf This paper modeled concurrent phenomena via higher dimensional transitions, formalized by directed or monoidal (as opposed to groupoidal) homotopy, nowadays called dihomotopy, represented in the case of my paper using n-categories. Eric Goubault and Thomas Jensen subsequently developed this notion in a homological framework, presenting "Homology of higher-dimensional automata" at CONCUR'92. Goubault then founded the GETCO (GEometric and Topological COmputation) series of conferences on higher dimensional automata and related geometric models, the seventh of which was held in San Francisco in 2005. Since then other geometric models besides n-categories have been used, although Philippe Gaucher has stuck with the n-category approach more faithfully even than myself (following a suggestion of Rob van Glabbeek I've drifted over to cubical complexes, the category of which is neatly definable as the topos Set^FinBip where FinBip is the category of finite bipointed sets---actually the free such suffice). Since the above POPL paper has 99 citations I suggest following those links forward in time (backward along the links) to see how the categorical aspects have been applied in the intervening 18 years and how the thinking along that homological/dihomotopic line has developed. Verification should not be thought of as simply manipulation of logical formulas, but should take into account the known algorithms for the data structures arising in the programs being verified. In the case of concurrent programs, especially for phenomena such as deadlock, higher dimensional automata supply core data structures for the concept. When the essence of deadlock is geometric, translating the concepts into a logical language and applying decision methods tailored to logic tends to hide the wood with the trees. Vaughan Pratt [For admin and other information see: http://www.mta.ca/~cat-dist/ ]