2026-08-20T15:34:37Zhttps://docta.ucm.es/rest/oai/request
oai:docta.ucm.es:20.500.14352/982542025-04-01T23:46:43Zcom_20.500.14352_14col_20.500.14352_15
Docta Complutense author Aceto, Luca author Della Monica, Dario author Fábregas, Ignacio author Ingólfsdóttir, Anna author Fábregas Alfaro, Ignacio 2024-02-02T12:25:27Z 2024-02-02T12:25:27Z 2018 L. Aceto, D. Della Monica, I. Fábregas, A. Ingólfsdóttir, When are prime formulae characteristic?, Theoretical Computer Science 777 (2019) 3–31. https://doi.org/10.1016/j.tcs.2018.12.004. 1879-2294 10.1016/J.TCS.2018.12.004 https://hdl.handle.net/20.500.14352/98254 https://doi.org/10.1016/J.TCS.2018.12.004 In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to various behavioural relations in the literature. In particular, characteristic formulae are exactly the prime and consistent ones for all the semantics in van Glabbeek’s linear time-branching time spectrum. eng When are prime formulae characteristic? journal article UGFyYSBxdWUgZWwgcmVwb3NpdG9yaW8gaW5zdGl0dWNpb25hbCBkZSBsYSBVbml2ZXJzaWRhZCBkZSBNYWRyaWQgcHVlZGEgYWxtYWNlbmFyIHkgZGlzdHJpYnVpciBlbCBvYmpldG8gZGlnaXRhbCBkZXBvc2l0YWRvLCBlcyBuZWNlc2FyaW8gcXVlIGxhIHBlcnNvbmEgcXVlIGhhZ2EgZWwgZGVww7NzaXRvIGxlYSB5IGFjZXB0ZSBsYXMgY29uZGljaW9uZXMgZXN0YWJsZWNpZGFzIGVuIGVzdGEgbGljZW5jaWE6CuKAoiBBY2VwdGFuZG8gZXN0YSBsaWNlbmNpYSwgdXN0ZWQgY29tbyBhdXRvci9yZXMgeS9vIHByb3BpZXRhcmlvL3MgZGUgbG9zIGRlcmVjaG9zIGRlIHByb3BpZWRhZCBpbnRlbGVjdHVhbCwgbyBsYSBwZXJzb25hIGRlbGVnYWRhIHBhcmEgaGFjZXJsbyAsIG90b3JnYSBhbCByZXBvc2l0b3JpbyBkZSBsYSBVbml2ZXJzaWRhZCBDb21wbHV0ZW5zZSBkZSBNYWRyaWQgZWwgZGVyZWNobyBubyBleGNsdXNpdm8gZGUgcmVwcm9kdWNjacOzbiB5IGRpc3RyaWJ1Y2nDs24gZGUgc3Ugb2JyYSBlbiBjdWFscXVpZXIgZm9ybWF0byB5IG1lZGlvLgrigKIgRWwgZGVwb3NpdGFudGUsIGVuIGNhc28gZGUgdW5hIG9icmEgY29uIG3DoXMgZGUgdW4gYXV0b3IsIGdhcmFudGl6YSBxdWUgbG8gaGFjZSByZXNwb25zYWJsZW1lbnRlIGVuIG5vbWJyZSB5IGNvbiBjb25zZW50aW1pZW50byBkZSBsb3MgZGVtw6FzIGF1dG9yZXMuCuKAoiBBY2VwdGEgcXVlIGVsIHJlcG9zaXRvcmlvIGRlIGxhIFVuaXZlcnNpZGFkIENvbXBsdXRlbnNlIGRlIE1hZHJpZCBwdWVkYSBjb25zZXJ2YXIgbcOhcyBkZSB1bmEgY29waWEgZGUgZXN0ZSBkb2N1bWVudG8geSwgc2luIGFsdGVyYXIgc3UgY29udGVuaWRvLCBjb252ZXJ0aXJsbyBhIGN1YWxxdWllciBmb3JtYXRvIGRlIGZpY2hlcm8sIG1lZGlvIG8gc29wb3J0ZSwgcGFyYSBwcm9ww7NzaXRvcyBkZSBzZWd1cmlkYWQgeSBwcmVzZXJ2YWNpw7NuLgrigKIgRGVjbGFyYSBxdWUgZWwgZG9jdW1lbnRvIGVzIHVuIHRyYWJham8gb3JpZ2luYWwgc3V5bywgbyBxdWUgZXMgbGEgcGVyc29uYSBkZWxlZ2FkYSBwYXJhIHJlYWxpemFyIGVsIGRlcMOzc2l0byB5LCBwb3IgdGFudG8sIGN1ZW50YSBjb24gbGEgcG90ZXN0YWQgcGFyYSBvdG9yZ2FyIGxvcyBkZXJlY2hvcyBjb250ZW5pZG9zIGVuIGVzdGEgbGljZW5jaWEuIFRhbWJpw6luIGRlY2xhcmEgcXVlIHN1IGRvY3VtZW50byBubyBpbmZyaW5nZSBsbyBlc3RhYmxlY2lkbyBlbiBsYSB2aWdlbnRlIGxlZ2lzbGFjacOzbiBkZSBwcm9waWVkYWQgaW50ZWxlY3R1YWwuCuKAoiBTaSBlbCBkb2N1bWVudG8gY29udGllbmUgbWF0ZXJpYWxlcyBkZSBsb3MgY3VhbGVzIG5vIHRpZW5lIGxvcyBkZXJlY2hvcyBkZSBhdXRvciwgZGVjbGFyYSBxdWUgaGEgb2J0ZW5pZG8gZWwgcGVybWlzbyBzaW4gcmVzdHJpY2Npw7NuIGRlbCBwcm9waWV0YXJpbyBwYXJhIG90b3JnYXIgYSBsYSBVbml2ZXJzaWRhZCBDb21wbHV0ZW5zZSBkZSBNYWRyaWQgbG9zIGRlcmVjaG9zIHJlcXVlcmlkb3MgcG9yIGVzdGEgbGljZW5jaWEsIHkgcXVlIGVzZSBtYXRlcmlhbCwgY3V5b3MgZGVyZWNob3Mgc29uIGRlIHRlcmNlcm9zLCBlc3TDoSBjbGFyYW1lbnRlIGlkZW50aWZpY2FkbyB5IHJlY29ub2NpZG8gZGVudHJvIGRlbCBjb250ZW5pZG8gZGVsIGRvY3VtZW50by4K4oCiIFNpIGVsIGRvY3VtZW50byBzZSBiYXNhIGVuIHVuYSBvYnJhIHF1ZSBoYSBzaWRvIHBhdHJvY2luYWRhIG8gYXBveWFkYSBwb3IgdW5hIGFnZW5jaWEgdSBvcmdhbml6YWNpw7NuIGRpZmVyZW50ZSBkZSBsYSBVbml2ZXJzaWRhZCBDb21wbHV0ZW5zZSBkZSBNYWRyaWQsIHVzdGVkIGRlY2xhcmEgcXVlIGhhIGN1bXBsaWRvIGNvbiBsYXMgb2JsaWdhY2lvbmVzIHJlcXVlcmlkYXMgcG9yIGVzdGUgY29udHJhdG8gbyBhY3VlcmRvLgrigKIgTGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkIGlkZW50aWZpY2Fyw6EgY2xhcmFtZW50ZSBzdS9zIG5vbWJyZS9zIGNvbW8gZWwvbG9zIGF1dG9yL2VzIG8gcHJvcGlldGFyaW8vcyBkZSBsb3MgZGVyZWNob3MgZGVsIGRvY3VtZW50bywgeSBubyBoYXLDoSBuaW5ndW5hIGFsdGVyYWNpw7NuIGRlIHN1IGRvY3VtZW50byBkaWZlcmVudGUgYSBsYXMgcGVybWl0aWRhcyBlbiBlc3RhIGxpY2VuY2lhLgrigKIgVHJhYmFqb3MgZGVwb3NpdGFkb3MgcG9yIHN1IHByb3BpbyBhdXRvcjogYWwgYXV0by1hcmNoaXZhciBlc3RhIGNvbGVjY2nDs24gZGUgZmljaGVyb3MgeSBtZXRhZGF0b3MgYmlibGlvZ3LDoWZpY29zIGFzb2NpYWRvcywgb3RvcmdvIGFsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwgZGUgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkIGVsIGRlcmVjaG8gcGFyYSBhbG1hY2VuYXJsb3MgeSBkaXN0cmlidWlybG9zLiBEZWNsYXJvIHF1ZSBlc3RlIG1hdGVyaWFsIGVzIGRlIG1pIHByb3BpZWRhZCBpbnRlbGVjdHVhbCB5IHF1ZSBlbCByZXBvc2l0b3JpbyBpbnN0aXR1dGljaW9uYWwgZGUgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkLCBubyBhc3VtZSByZXNwb25zYWJpbGlkYWQgYWxndW5hIGVuIGNhc28gZGUgcXVlIHNlIHByb2R1emNhIHVuYSB2aW9sYWNpw7NuIGRlIGRlcmVjaG9zIGRlIHByb3BpZWRhZCBhbCBkaXN0cmlidWlyIGVzdG9zIGZpY2hlcm9zIG8gbWV0YWRhdG9zLgrigKIgVHJhYmFqb3MgZGVwb3NpdGFkb3MgcG9yIG90cm9zIHF1ZSBubyBzZWFuIHN1IGF1dG9yOiBkZWNsYXJvIHF1ZSBsb3MgbWV0YWRhdG9zIGJpYmxpb2dyw6FmaWNvcyBxdWUgZXN0b3kgYXJjaGl2YW5kbyBlbiBlbCByZXBvc2l0b3JpbyBpbnN0aXR1Y2lvbmFsIGRlIGxhIFVuaXZlcnNpZGFkIENvbXBsdXRlbnNlIGRlIE1hZHJpZCwgc29uIGRlIGRvbWluaW8gcMO6YmxpY28uIFNpIG5vIGZ1ZXNlIGVsIGNhc28sIGFjZXB0byBwbGVuYSByZXNwb25zYWJpbGlkYWQgcG9yIGN1YWxxdWllciBpbmZyYWNjacOzbiBkZSBkZXJlY2hvcyBkZSBhdXRvciBxdWUgY29ubGxldmUgbGEgZGlzdHJpYnVjacOzbiBkZSBlc3RvcyBmaWNoZXJvcyBvIG1ldGFkYXRvcy4K4oCiIFBvciB0YW50bywgdG9kb3MgbG9zIG1ldGFkYXRvcyBwdWJsaWNhZG9zIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwgZGUgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkLCBlc3TDoW4gZGlzcG9uaWJsZXMgY29uIGxhIGxpY2VuY2lhIENyZWF0aXZlIENvbW1vbnMgQ0MwIDEuMCBVbml2ZXJzYWwgT2ZyZWNpbWllbnRvIGFsIERvbWluaW8gUMO6YmxpY28gKENDMCAxLjApLiBFc3RhIGxpY2VuY2lhIHBlcm1pdGUgY29waWFyLCBtb2RpZmljYXIsIGRpc3RyaWJ1aXIsIHJldXRpbGl6YXIgeSBjb21wYXJ0aXIgcMO6YmxpY2EgeSBsaWJyZW1lbnRlIGxvcyBtZXRhZGF0b3MgKGluY2x1eWVuZG8gc3UgdXNvIGNvbWVyY2lhbCksIHNpbiB0ZW5lciBxdWUgcGVkaXIgcGVybWlzby4gU2kgdGVyY2VyYXMgcGFydGVzIHVzYW4gZXN0b3MgbWV0YWRhdG9zLCBkZWJlbiBoYWNlciB1biByZWNvbm9jaW1pZW50byB5IHVuYSBhdHJpYnVjacOzbiBhIGxhcyBmdWVudGVzIGRlIGxvcyBtaXNtb3MuIExhIHJldXRpbGl6YWNpw7NuIGRlIGVzdG9zIG1ldGFkYXRvcyB0YW1iacOpbiBlcyBsaWJyZSwgdGFsIHkgY29tbyBlc3RhYmxlY2UgbGEgbGljZW5jaWEgZGUgdXNvIENDMC4K URL https://docta.ucm.es/bitstreams/6fb21749-5900-41e9-996e-d90d9eca9f4e/download File MD5 4fb749ff46f6f3dd93c4cc272fe5b197 626017 application/pdf Prime_formulae_characteristic.pdf URL https://docta.ucm.es/bitstreams/ab659d0b-398c-4544-a327-1359a40f765a/download File MD5 d7935baa89fd6fdad48831a4ef0368c5 125903 text/plain fabregas_when.pdf.txt