Decidable Fragments of a Higher Order Calculus with Locations | Zendy

Mikkel Bundgaard | Zendy; Jens Chr. Godskesen | Zendy; Bjørn Haagensen | Zendy; Hans Hüttel | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Decidable Fragments of a Higher Order Calculus with Locations

Author(s) -

Mikkel Bundgaard,

Jens Chr. Godskesen,

Bjørn Haagensen,

Hans Hüttel

Publication year - 2009

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2009.06.016

Subject(s) - undecidable problem , decidability , process calculus , reachability , pi calculus , property (philosophy) , mathematics , bounding overwatch , calculus (dental) , fragment (logic) , reachability problem , first order , discrete mathematics , computer science , algebra over a field , algorithm , pure mathematics , theoretical computer science , artificial intelligence , medicine , philosophy , epistemology , dentistry

Homer is a higher order process calculus with locations. In this paper we study Homer in the setting of the semantic finite control property, which is a finite reachability criterion that implies decidability of barbed bisimilarity. We show that strong and weak barbed bisimilarity are undecidable for Homer. We then identify and compare two distinct subcalculi of Homer that both satisfy the semantic finite control property. One subcalculus is obtained by using a type system bounding the size of process terms. The other subcalculus is obtained by considering the image of the encoding of the finite control @p-calculus in Homer.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research