On the axiomatizability of impossible futures

Article

Chen, T., Fokkink, W. and Van Glabbeek, R. 2015. On the axiomatizability of impossible futures. Logical Methods in Computer Science. 11 (3), pp. 1-30. https://doi.org/10.2168/LMCS-11(3:17)2015
TypeArticle
TitleOn the axiomatizability of impossible futures
AuthorsChen, T., Fokkink, W. and Van Glabbeek, R.
Abstract

A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves omega-completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and omega-complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a finite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a finite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no finite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is infinite, then the aforementioned ground-complete axiomatizations are shown to be omega-complete. If the alphabet is finite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a finite basis.

Research GroupFoundations of Computing group
JournalLogical Methods in Computer Science
ISSN1860-5974
Publication dates
Print22 Sep 2015
Publication process dates
Deposited03 Jun 2015
Submitted04 Jan 2015
Output statusPublished
Accepted author manuscript
Additional information

Article number = Paper 17

Web address (URL)https://lmcs.episciences.org/1593
Digital Object Identifier (DOI)https://doi.org/10.2168/LMCS-11(3:17)2015
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/85895

Log in to edit

Download files

Accepted author manuscript
lmcs15.pdf

  • 80
    total views
  • 15
    total downloads
  • 1
    views this month
  • 1
    downloads this month

Export as

Related outputs

Augmenting bug localization with part-of-speech and invocation
Zhou, Y., Tong, Y., Chen, T. and Han, J. 2017. Augmenting bug localization with part-of-speech and invocation. International Journal of Software Engineering and Knowledge Engineering. 27 (06), pp. 925-949. https://doi.org/10.1142/s0218194017500346
Formal reasoning on infinite data values: an ongoing quest
Chen, T., Song, F. and Wu, Z. 2017. Formal reasoning on infinite data values: an ongoing quest. SETSS 2016: Second International School Engineering Trustworthy Software Systems, Tutorial Lectures. Chongqing, China 28 Mar - 02 Apr 2016 Springer. pp. 195-257 https://doi.org/10.1007/978-3-319-56841-6_6
ProEva: runtime proactive performance evaluation based on continuous-time markov chains
Su, G., Chen, T., Feng, Y. and Rosenblum, D. 2017. ProEva: runtime proactive performance evaluation based on continuous-time markov chains. 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE). Buenos Aires, Argentina 20 - 28 May 2017 Institute of Electrical and Electronics Engineers (IEEE). pp. 484-495 https://doi.org/10.1109/ICSE.2017.51
Analyzing APIs documentation and code to detect directive defects
Zhou, Y., Gu, R., Chen, T., Huang, Z., Panichella, S. and Gall, H. 2017. Analyzing APIs documentation and code to detect directive defects. 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE). Buenos Aires, Argentina 20 - 28 May 2017 Institute of Electrical and Electronics Engineers (IEEE). pp. 27-37 https://doi.org/10.1109/ICSE.2017.11
Model based analysis of insider threats
Chen, T., Han, T., Kammueller, F., Nemli, I. and Probst, C. 2016. Model based analysis of insider threats. 2016 International Conference on Cyber Security and Protection of Digital Services (Cyber Security). London, United Kingdom 13 - 14 Jun 2016 Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/CyberSecPODS.2016.7502350
A proof-theoretic trust and reputation model for VANET
Primiero, G., Raimondi, F., Chen, T. and Nagarajan, R. 2017. A proof-theoretic trust and reputation model for VANET. S4CIP’17: 2nd Workshop on Safety & Security aSSurance for Critical Infrastructures Protection. Paris, France 29 Apr 2017 Institute of Electrical and Electronics Engineers (IEEE). pp. 146-152 https://doi.org/10.1109/EuroSPW.2017.64
The packing chromatic number of the infinite square lattice is between 13 and 15
Martin, B., Raimondi, F., Chen, T. and Martin, J. 2017. The packing chromatic number of the infinite square lattice is between 13 and 15. Discrete Applied Mathematics. 225, pp. 136-142. https://doi.org/10.1016/j.dam.2017.03.013
Towards a novel approach for defect localization based on part-of-speech and invocation
Tong, Y., Zhou, Y., Fang, L. and Chen, T. 2015. Towards a novel approach for defect localization based on part-of-speech and invocation. Internetware 2015: 7th Asia-Pacific Symposium on Internetware. Wuhan, China 06 Nov 2016 Association for Computing Machinery (ACM). pp. 52-61 https://doi.org/10.1145/2875913.2875919
Analyzing eventual leader election protocols for dynamic systems by probabilistic model checking
Gu, J., Zhou, Y., Wu, W. and Chen, T. 2015. Analyzing eventual leader election protocols for dynamic systems by probabilistic model checking. First International Conference on Cloud Computing and Security (ICCCS 2015). Nanjing, China 13 - 15 Aug 2015 Springer. pp. 192-205 https://doi.org/10.1007/978-3-319-27051-7_17
A complete decision procedure for linearly compositional separation logic with data constraints
Gu, X., Chen, T. and Wu, Z. 2016. A complete decision procedure for linearly compositional separation logic with data constraints. IJCAR 2016: 8th International Joint Conference on Automated Reasoning. University of Coimbra, Portugal 27 Jun - 02 Jul 2016 Springer. pp. 532-549 https://doi.org/10.1007/978-3-319-40229-1_36
A computationally grounded, weighted doxastic logic
Chen, T., Primiero, G., Raimondi, F. and Rungta, N. 2016. A computationally grounded, weighted doxastic logic. Studia Logica. 104 (4), pp. 679-703. https://doi.org/10.1007/s11225-015-9621-4
An iterative decision-making scheme for Markov decision processes and its application to self-adaptive systems
Su, G., Chen, T., Feng, Y., Rosenblum, D. and Thiagarajan, P. 2016. An iterative decision-making scheme for Markov decision processes and its application to self-adaptive systems. 19th International Conference Fundamental Approaches to Software Engineering (FASE 2016). Eindhoven, The Netherlands 02 - 08 Apr 2016 Springer. pp. 269-286 https://doi.org/10.1007/978-3-662-49665-7_16
Asymptotic perturbation bounds for probabilistic model checking with empirically determined probability parameters
Su, G., Feng, Y., Chen, T. and Rosenblum, D. 2016. Asymptotic perturbation bounds for probabilistic model checking with empirically determined probability parameters. IEEE Transactions on Software Engineering. 42 (7), pp. 623-639. https://doi.org/10.1109/TSE.2015.2508444
Verifying pushdown multi-agent systems against strategy logics
Chen, T., Song, F. and Wu, Z. 2016. Verifying pushdown multi-agent systems against strategy logics. IJCAI 2016: 25th International Joint Conferences on Artificial Intelligence (IJCAI). New York, New York, USA 09 - 15 Jul 2016 AAAI Press / International Joint Conferences on Artificial Intelligence. pp. 180-186
Global model checking on pushdown multi-agent systems
Chen, T., Song, F. and Wu, Z. 2016. Global model checking on pushdown multi-agent systems. Thirtieth AAAI Conference on Artificial Intelligence (AAAI-16). Phoenix, Arizona, USA 12 - 17 Feb 2016 Association for the Advancement of Artificial Intelligence (AAAI). pp. 2459-2465 https://doi.org/10.1609/aaai.v30i1.10124
On the complexity of computing maximum entropy for Markovian models
Chen, T. and Han, T. 2014. On the complexity of computing maximum entropy for Markovian models. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014. New Delhi, India 15 - 17 Dec 2014 Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. pp. 571-583
On the total variation distance of labelled Markov chains
Chen, T. and Kiefer, S. 2014. On the total variation distance of labelled Markov chains. Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - CSL-LICS 2014. Vienna, Austria 14 - 18 Jul 2014 Association for computing machinery. https://doi.org/10.1145/2603088.2603099
Perturbation analysis in verification of discrete-time Markov chains
Chen, T., Feng, Y., Rosenblum, D. and Su, G. 2014. Perturbation analysis in verification of discrete-time Markov chains. 25th Conference on Concurrency Theory (CONCUR 2014). Rome, Italy 02 - 05 Sep 2014 Springer. https://doi.org/10.1007/978-3-662-44584-6_16
Continuous-time orbit problems are decidable in polynomial-time
Chen, T., Yu, N. and Han, T. 2015. Continuous-time orbit problems are decidable in polynomial-time. Information Processing Letters. 115 (1), pp. 11-14. https://doi.org/10.1016/j.ipl.2014.08.004
A probabilistic analysis framework for malicious insider threats
Chen, T., Kammueller, F., Nemli, I. and Probst, C. 2015. A probabilistic analysis framework for malicious insider threats. 3rd International Conference on Human Aspects of Information Security, Privacy and Trust, HAS 2015, held as part of HCI International 2015. Los Angeles, California, USA 02 - 07 Aug 2015 Springer. pp. 178-189
Quantitative verification of implantable cardiac pacemakers over hybrid heart models
Chen, T., Diciolla, M., Kwiatkowska, M. and Mereacre, A. 2014. Quantitative verification of implantable cardiac pacemakers over hybrid heart models. Information and Computation. 236, pp. 87-101. https://doi.org/10.1016/j.ic.2014.01.014
On the satisfiability of indexed linear temporal logics
Chen, T., Song, F. and Wu, Z. 2015. On the satisfiability of indexed linear temporal logics. 26th International Conference on Concurrency Theory, CONCUR 2015. Madrid, Spain 01 - 04 Sep 2015 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH. pp. 254-267 https://doi.org/10.4230/LIPIcs.CONCUR.2015.254
Ready to preorder: the case of weak process semantics
Chen, T., Fokkink, W. and Van Glabbeek, R. 2008. Ready to preorder: the case of weak process semantics. Information Processing Letters. 109 (2), pp. 104-111. https://doi.org/10.1016/j.ipl.2008.09.003
On the axiomatizability of priority II
Aceto, L., Chen, T., Ingolfsdottir, A., Luttik, B. and Van de Pol, J. 2011. On the axiomatizability of priority II. Theoretical Computer Science. 412 (28), pp. 3035-3044. https://doi.org/10.1016/j.tcs.2011.02.033
On finite alphabets and infinite bases
Chen, T., Fokkink, W., Luttik, B. and Nain, S. 2008. On finite alphabets and infinite bases. Information and Computation. 206 (5), pp. 492-519. https://doi.org/10.1016/j.ic.2007.09.003
Model checking of continuous-time Markov chains against timed automata specifications
Chen, T., Han, T., Katoen, J., Mereacre, A. and Jagadeesan, R. 2011. Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods in Computer Science. 7 (1). https://doi.org/10.2168/LMCS-7(1:12)2011
Automatic verification of competitive stochastic systems
Chen, T., Forejt, V., Kwiatkowska, M., Parker, D. and Simaitis, A. 2013. Automatic verification of competitive stochastic systems. Formal Methods in System Design. 43 (1), pp. 61-92. https://doi.org/10.1007/s10703-013-0183-7