Nadia Ben Amor

Marie-Catherine Heitz

RASPT2 study of the valence excited states of an iron-porphyrin-carbonyl model complex

Keywords: RASPT2, IPEA, Metalloporphyrin, Iron, Excited states

Multireference wavefunction calculations of the singlet valence excited states of an iron-porphyrin-pyrazine-carbonyl complex up to the Soret band (about 3 eV) are presented. This complex is chosen to be a model for the active site of carboxyhemoglobin/myoglobin. The investigations are performed at the Restricted Active Space Second Order Perturbation (RASPT2) level involving an extended active space on the porphyrin ligand in addition to the active orbitals needed for the description of the metal-ligand interactions. Metal-to-Ligand-Charge-Transfer states d → π * and some Metal-Centered d → d transitions are found in the lowest part of the spectrum, below the first π → π * intraporphyrin transitions (Q band). Doubly excited states involving simultaneous intraporphyrin and metal centered excitations are found in the vicinity of the second set of intraporphyrin transitions (the so-called Soret band). The effect of the extension of the active space on the porphyrin ligand beyond the Gouterman's orbitals set is investigated together with the effect of inclusion of the Ionization Potential Electronic Affinity (IPEA) shift in the RASPT2 treatment.

INTRODUCTION

Metalloporphyrins are playing an important role in fundamental processes in biological functions like oxygen transport and activation 1 or in biomimetic catalysis 2,3 . They can also be photoactivated through the excitation of the strongly absorbing porphyrin ring in the visible or ultra-violet region. The presence of an extended π-conjugated chromophore and of a metallic center leads to a variety of dynamical processes such as charge transfer, dissociation of axial ligands, internal conversion and intersystem crossings. These excited state processes can be studied in a biological environment 4,5 , in the condensed 6 or gas 7 phases.

In this work, we focus on an iron-porphyrin complex with two axial ligands, namely a carbonyl and a pyrazine (pz) ligand. This FeP(pz)CO complex is considered as a model for the active site of carboxyhemoglobin or carboxymyoglobin. Hemoglobin and myoglobin are well known for performing the transport and the storage of O 2 , but they can also bind other small molecules such as CO or NO. In the case of CO, the interaction with IR-light can be used experimentally to probe the ligand transfer inside the protein [8][9][10] or to perform vibrational ladder climbing 11 to populate high vibrational excited states. From the theoretical side, various molecular processes have been studied: photodissociation mechanism of CO [12][13][14] , dynamics of spin transitions 14 and vibrational dynamics 15,16 . In this paper, we present Restricted and Complete Active Space Second Order Perturbation RASPT2 17 and CASPT2 18 calculations of the valence singlet excited states (until ≈ 3 eV) of the FeP(pz)CO complex. Compared to the standard model used for representing the active site of either hemoglobin or myoglobin, we replace the imidazole (C 3 H 4 N 2 ) group by a pyrazine (C 4 H 4 N 2 ) group, leading to a complex of C 2v symmetry. This reduces the number of states in each irreducible representation, making the calculations more tractable. Indeed, iron-porphyrins are so-called irregular porphyrins where the partially filled d-shell contributes significantly to the excited state spectrum through excitations from or to metallic orbitals. Thus, the challenge is the balanced description of the two subsystems (the porphyrin π system and the 3d-shell of the iron) to describe in a consistent way the various excitations of the valence spectrum: Metal-Centered (MC) and Metal-to-Ligand-Charge-Transfer (MLCT) transitions, intra-porphyrin excitations and mixed double excitations. Excited states involving excitations to the pyrazine ligand are not investigated in the present work. The metallic site of carboxy-hemoglobin/myoglobin is experimentally assigned to a diamagnetic ground state (see for instance Refs 19 and20 ). This can be rationalized on the basis of the strong ligand field of CO 21 . We thus focus on singlet excited states .

Multireference perturbative methods are commonly used for calculations of excited states (see recent review in ref 22 ). The introduction of dynamical correlation thanks to methods like CASPT2 in 1990 and then RASPT2 in 2008 represented an important step towards the study of excited states of large systems. In 2004, a modification of the zeroth-order Hamiltonian in the CASPT2 and then in the RASPT2 methods was proposed to compensate an unbalanced treatment of closed and open shells 23 . The so-called Ionization Potential Electronic Affinity (IPEA) shift, a single parameter whose numerical value (0.25 a.u.) was selected from benchmark calculations, was supposed to be systematically used from then on 23 . More recently, discussions about the use of IPEA, and its specific numerical value, have appeared in the literature, concerning organic systems in general 24,25 , iron compounds 26,27 and free-based and regular porphyrins 28 in particular. In the present work, calculations with and without the use of the IPEA shift are compared. The second aspect we wish to highlight in this work is the composition of the active space on the porphyrin ligand.

Gouterman, in the 1960s, rationalized the absorption spectra of porphyrins on the basis of one-electron transitions between the four frontier orbitals of the conjugated cycle 29,30 .

In our previous study 31 , the active space on the porphyrin was restricted to this so-called Gouterman's set. Taking also into account all the orbitals required for the description of the iron and the metal-ligand interactions according to standard rules [32][33][34] , we reported CASPT2 calculations based on a 14 electrons in 14 active orbitals space 31 . In the present work, we present RASPT2 calculations including an extended active space on the porphyrin, beyond the four Gouterman's frontier orbitals and we discuss the effect of the IPEA shift in connection with the enlargement of the active space.

COMPUTATIONAL METHODS

Computational details

The calculations were performed at the same geometry as the previous CASPT2 study 31 . This structure of C 2v symmetry is displayed in Figure 1 and Cholesky decomposition technique was used to reduce the number of integrals 40,41 . The number of roots in the state-average CASSCF and RASSCF calculations varied according to the symmetry. The description of the singlet states up to the Soret Band required 5 roots for the A 2 symmetry, 8 roots of the B 1 and B 2 symmetries, while excited states of calculated considering an electronic ground state energy calculated with the same number of roots as for the excited states. Core electrons were frozen except the 3s and 3p electrons of the iron atom which were correlated. A common level shift value of 0.4 a.u. was used for all the calculations. The calculations were performed with standard IPEA value of 0.25 a.u. and without IPEA shift. The oscillator strengths were calculated thanks to the restricted active space state interaction approach (RASSI) 42 .

Choice of active spaces

The full set of valence π and π * orbitals of the porphyrin together with the 3d-iron orbitals and the orbitals describing the metal-ligands interaction would constitute a 36 electrons in 36 orbitals active space. This exceeds by far the feasibility of CASSCF 43 . RASSCF is considered instead, which implies the partition of an active space in RAS1, RAS2 and RAS3 subspaces 44 . The validity of the partition must be checked with respect to the strongest correlation effects (possible strong covalent metal-ligand bonding effects and 3d doubleshell effect in case of first-row transition metals) and to the orbitals becoming partially occupied through the electronic excitations 34 . We aim at describing the valence excited states until ≈ 3 eV that means Metal Centered (MC) transitions (d → d), Metal-to-Ligand-Charge-Transfer (MCLT) states (d → π * ), Ligand-to-Metal-Charge-Transfer (LMCT) states (π → d), and intra-porphyrin excitations (π → π * ). We include in the RAS2 space, where all possible excitations are allowed, all the orbitals becoming singly occupied in at least one of the main determinants of these states, leading to a set of nine orbitals, namely the five 3d orbitals of the iron and the four Gouterman's orbitals which consist of the four frontier orbitals of the porphyrin ring (two occupied and two unoccupied). The orbitals of the RAS2 space obtained after an eight roots state averaged RASSCF for the A 1 symmetry, can be found in Figure 2, with their occupation in the electronic ground state. Further active orbitals are included in the RAS1 and RAS3 space where at most two holes and two particules are allowed. The composition of these spaces follows two goals : first the proper description of the iron and of the metal-ligand interaction and second a good description of the π system of the porphyrin ring. The first goal is reached by including in the RAS1 space two metal-ligand σ-bonding orbitals, counterpart of the 3d ground state empty iron orbitals, and in the RAS3 space the three 3d ′ double shell orbitals correlating the three 3d ground state occupied orbitals. This leads to a 14 electrons in 14 orbitals active space, referred to as the small active space, matching the active space of the previous CASPT2 study 31 . A comparison of the RASPT2/CASPT2 results for this small active space enables the assessment of including the σ and 3d ′ orbitals only in a RAS1 or a RAS3 space, i.e. restricting the number of excitations from or into these orbitals. This will be discussed in the next subsection. Concerning the description of the porphyrin, due to the size of the RAS2 space, it is not possible to include all the remaining orbitals of the porphyrin π system. In practice, in addition to the four π orbitals of the RAS2 space, the 7 next highest occupied π orbitals are added to the RAS1 space and 5 virtual π * orbitals are added to the RAS3 space, leading to a 28 electrons in 26 orbitals active space. This is equivalent to exclude the contribution of the β carbons of the pyrrole rings to the porphyrin π system, as has been done by Pierloot and coworkers 45 . The number of determinants in the total RASSCF space is about 35 millions of determinants. Plots of the RAS1 and RAS3 can also be found in This 28e26a active space is already large and is designed to describe the metal center and the porphyrin π system. We do not include orbitals of the π system of the pyrazine group in the active spaces. Thus, electronic states involving excitations on the pyrazine ligand cannot be obtained by our calculations and are ignored in the present study. The (3s3p) correlation effect has been shown to be important in the spin state energetics of first-row transition metal complexes as discussed by Pierloot and collaborators 46,47 . In this work, we handle transition energies between states of same spin. The effect of (3s3p) correlation on the d-d transitions has been checked at the CASPT2 level, using a metallic-only active space, by including or not these orbitals in the active space. The results are presented in the supplementary material file (Table S2). The mean value of the differences on the transition energies with and without adding the 3s and 3p orbitals in the active space is of 0.1 and 0.06 eV without and with IPEA respectively. The effect is then small and only weakly dependent on the IPEA shift. These orbitals are not included in the RASSCF active space.

Comparison of CASPT2 and RASPT2 results for the 14e14a active space

The purpose of this subsection is to validate the transfer of some orbitals involved in the description of the metal or of the metal-ligand interaction from RAS2 to either RAS1 or RAS3 by comparing CASPT2 and RASPT2 results obtained with the same 14e14a active space. The electronic states issued from state-average CASSCF and RASSCF calculation can be clearly identified with the nature of the dominant configurations such as d → d , π → π * states etc... The detailed description of the electronic excited states of the targeted complex will be presented in the next section. Table S3 in the Supplementary Material gives the difference between CASPT2-14e14a and RASPT2-14e14a calculation. The transition energies obtained at the RASPT2 level are systematically underestimated with respect to the CASPT2 ones, with a mean difference of 0.12 eV. Only two transition energies show a deviation larger than 0.16 eV, namely 0.37 and 0.38 eV. They correspond to the d → π * states of B 1 and B 2 symmetries. In their respective symmetry, they are the only states with a d 5 configuration of the iron, the seven other states having a d 6 configuration. The orbitals, being optimized through a state-averaged procedure, might be less adapted to a d 5 configuration of the iron. A bias in the description of these two d → π * states is thus possible and a restriction of possible excitations when going from CASSCF to RASSCF might further affect the transition energies. The difference is less important in case of the d → π * states of A 1 and A 2 symmetries where 3-roots and 5-roots state-averaged calculations have been performed. In these cases, the deviations between the CASPT2-14e14a and the RASPT2-14e14a results range from 0.06 to 0.12 eV. For the d → d states which are directly concerned by the restriction of the excitations, the deviations are on average of 0.085 eV. As a conclusion, the inclusion of the σ orbitals in RAS1 and of the 3d ′ orbitals in RAS3, allowing at most double excitations out of or in these spaces, is a reasonable strategy leading, in the great majority of cases, to errors in the transition energies ranging from 0.02 to 0.16 eV.

RESULTS and DISCUSSION

Excited states of the iron-porphyrin-pyrazine-carbonyl complex

The transition energies, the oscillator strengths together with the electronic nature of the excited states of the FeP(pz)CO complex obtained from the RASPT2-28e26a calculation, without and with standard IPEA shift, are presented in Table 1. The different states are labelled and listed in the increasing energy order issued from the calculation without inclusion of the IPEA shift. We first discuss the electronic spectrum obtained without IPEA shift. The transition energies of the six states range from 1.76 to 2.21 eV. MLCT states involving charge transfer to the CO are not investigated here. In the previous CASPT2 study 31 , with the appropriate active space, a first d → π * CO state was found at about 4.0 eV. Pure doubly excited states are found starting from 2.8 eV. They result from simultaneous mono-excitations on both the iron center and the porphyrin ring. The lowest of these states are located about 2.8-3.0 eV above the electronic ground state in the vicinity of the Soret states.

a 1 B d x 2 -
They are based on the first MC transition (d x 2 -y 2 →d xy ). The occurrence of such rather lowlying doubly excited states among the valence excited states comes from the large conjugated π system of the porphyrin ligand which results in a small HOMO-LUMO intra-ligand gap and could be specific to partially filled d-shell metalloporphyrins. Two other doubly excited states are reported at energies above 3.0 eV. Another group of states, characterised by a mixed character of LMCT (π →d) and mixed double excitations, can be found around 2.70 eV.

Effect of the enlargement of the active space on the porphyrin ligand beyond the Gouterman's set

In this subsection we discuss the effect of extending the active space on the porphyrin beyond the four Gouterman orbitals. Investigations based on a DFT/MRCI treatment have concluded to the necessity to go beyond the Gouterman four-orbitals picture for the description of the Soret band, especially for the free-base porphyrin 50 . We present in Table 2 the transition energies obtained for the FeP(pz)CO complex at the CASPT2 level with the 14e14a active space. The signed differences between the RASPT2-28e26a and the CASPT2-14e14a transition energies without IPEA shift are reported in Table S4 of the Supplementary Material. The weights of the main configurations are similar in the RASSCF and CASSCF calculations, allowing for such a comparison. These differences in transition energies are small for the MC states with a mean unsigned difference of 0.14 eV. This is only slightly larger than the mean difference of 0.085 eV observed when comparing CASPT2-14e14a and RASPT2-14e14a, showing that, as expected, for d-d transitions, the inclusion of only the Gouterman set in the active space is sufficient. The inclusion of 12 additional orbitals of the π system in either the RAS1 or the RAS3 space has a larger but still moderate effect

a 1 B d x 2 -
d yz π a 1 →d xy π * b 2 0.12 d xz π a 1 →d xy π * b 1 0.12 Table 2: CASPT2(14e14a).
Transition energies of the FeP(pz)CO complex, together with the oscillator strengths and the configurations with weights larger than 0.10, calculated at the CASPT2 level with the 14e14a active space, with values of IPEA shift of 0. and 0.25 a.u.

The excited states are listed in the increasing energy order obtained without IPEA shift.

Their labels correspond to those attributed following to the RASPT2-28e26a calculation. on the MLCT states: 0.20 eV on average, with a maximum of 0.29 eV. The largest effect is observed for the two states corresponding to the Q band namely the first intraporphyrin excited states c 1 B 1 and c 1 B 2 , for which the extension of the active space increases the transition energies from 1.69 eV to 2.31 eV and 1.71 eV to 2.30 eV respectively. Thus for the Q band, the extension of the active space significantly improves the agreement with experiment (2.18-2.30 eV). The effect on the Soret band is limited to 0.30 eV but the agreement with experiment is also improved by the enlargement. Three orbitals can be distinguished among the porphyrin π system, in addition to the Gouterman orbitals, as playing a role at the non-dynamical correlation level. The 30b 1 and 25b 2 orbitals of the RAS1 space and the 48a 1 orbital of the RAS3 space (see Figure 2) are singly occupied in several determinants with weights of the order of 0.5 to 1% in the wavefunction development of the Q and Soret states.

Configurations

For pure doubly excited states, the enlargement of the active space increases the transition energies of an amount of 0.20 to 0.55 eV. Concerning LMCT-doubly excited states, the effect is moderate, at most of 0.18 eV.

Effect of IPEA shift

The effect of inclusion of the IPEA shift in the RASPT2-28e26a can be analysed from Table 1 and from Table S5 (Supplementary Material) which reports the difference between transition energies computed with and without IPEA shift, for all the excited states sorted by electronic character and symmetry. The smallest effect is seen on the d-d transition energies with a mean difference of 0.28 eV, while the effect is a little bit larger for the MLCT states (0.38 eV on average). These increases of transition energies are similar to those reported in the original publication introducing the IPEA shift 23 , where values ranging from about 0. IPEA shift is the fact that some doubly excited states, based on the lowest d-d transition, are nearly degenerated with the intraporphyrin excitations forming the strongly absorbing Soret band. Also, the states with Ligand-to-Metal-Charge-Transfer (π →d) character lie below the Soret band.

The effect of the inclusion of the IPEA in the CASPT2-14e14a calculation, where the active orbitals on the porphyrin ligand are limited to the Gouterman's set, is pointed out in Table S6 of the Supplementary Material. The effect on the d-d states is nearly identical to the one observed for the large active space (0.29 eV on average) but the introduction of the IPEA shift increases the transition energies of states involving intraporphyrin excitation of about 1 eV. This very large effect of IPEA on the transition energies of theses states with a 14e14a active space was already emphasized in our previous work 31 . The present calculation shows that the inclusion of π orbitals of the porphyrin ring beyond the Gouterman's set in the active space significantly reduces the effect of the IPEA shift (from about 1 eV to 0.5 eV)

and keeps the effect in more usual values.

In Table 3 are collected together the RASPT2-28e26a and CASPT2-14e14a transition energies without and with IPEA, for the Q band and the Soret band together with the nearest available experimental results 48 . The small difference between the RASPT2-28e26a and CASPT2-14e14a results obtained with the standard IPEA suggests that the truncation of the active space is hidden by the use of the IPEA shift. The RASPT2 results for the Q band and the Soret band are very close to the experimental results as long as the IPEA shift is omitted. Inclusion of standard IPEA in the RASPT2 deteriorates this good agreement. This finding corroborates the conclusion of the RASPT2 calculations of Kerridge 28 on regular metalloporphyrins with either magnesium or zinc as central atom. In this work, where the entire π orbitals system was included in the active space, experimental transition energies were best reproduced by RASPT2 calculations without inclusion of IPEA shift 28 .

More generally, a recent work about the use of IPEA on the transition energies of organic systems has concluded that the introduction of IPEA was in fact not needed 24 . Our work points out that the dependence of the transition energies on the IPEA should be further investigated and particularly in case of large effects. A connection with a possible truncation of the active space should than be investigated.

CONCLUSIONS

Calculations of the singlet valence excited states of an iron-porphyrin-pyrazine-carbonyl complex up to the Soret band (about 3 eV) are presented. This complex has at the same time an organic chromophore and a metallic center absorbing both in the same energy range. The

  (plotted with MacMolPlt 35 ). The N(pyrazine)-Fe-C-O chain is chosen to lie along the z-axis while the Fe-N(porphyrin) bonds are bisectors of the xz and yz planes. The coordinates can be found in the Supplementary Material of Ref 31 . As expected considering the strong ligand field of CO and the d 6 configuration of the iron, the electronic ground state of the complex is a closed-shell singlet. The results of the geometry optimizations of other spin states based on DFT calculations are summarized in the Supplementary Material.

Figure 1 :

 1 Figure 1: Iron center in a porphyrin (P), with CO and pyrazine (pz) as axial ligands (FeP(pz)CO)

Figure 2 .

 2 Figure 2.

Figure 2 :

 2 Figure 2: Active orbitals obtained after an eight roots state averaged RASSCF-28e26a calculation of A 1 symmetry for the FeP(pz)CO complex.

  investigations are performed at the RASPT2 level involving an extended active space on the porphyrin ligand (16 π orbitals) in addition to the 10 active orbitals needed for the description of the metal-ligands interactions, leading to a total active space of 28 electrons in 26 orbitals. The variety of excited states to be considered (charge transfer states, metal centered and intraporphyrin excitations) leads to a RAS2 space of 9 orbitals. MLCT states d → π * and some MC d → d transitions are found in the lowest part of the spectra, below the first π → π * intraporphyrin transitions (Q band). Doubly excited states involving simultaneous intraporphyrin and metal-centered excitations, together with porphyrin-to-metal contributions, are found in the vicinity of the second intraporphyrin excitations, namely the strongly

Table 1 :

 1 y 2 →π * RASPT2(28e26a). Transition energies of the FeP(pz)CO complex, together withB d x 2 -y 2 π a 1 →d xy π * B d x 2 -y 2 π a 1 →d xy π * B d x 2 -y 2 π a 2 →d xy π * B d x 2 -y 2 π a 2 →d z 2 π * B d x 2 -y 2 π a 2 →d z 2 π *

		b 2	0.55	1.76 (0.0021)	2.10
	a 1 B	d x 2 -y 2 →π * b 1	0.54	1.77 (0.0021)	2.11
	a 1 A	d x 2 -y 2 →d xy	0.70	1.83 (0.0000)	1.98
	b 1 A	d xz →π * b 1	0.35	1.90 (0.6 10 -5 )	2.36
		d yz →π * b 2	0.32
	b 1 A	d yz →π * b 1	0.58	2.08 (0.0000)	2.40
	c 1 A	d xz →π * b 2	0.56	2.10 (0.0000)	2.44
	c 1 A	d yz →π * b 2	0.30	2.21 (0.7 10 -5 )	2.68
		d xz →π * b 1	0.27
	b 1 B	d yz →d z 2	0.56	2.22 (0.0008)	2.48
		d xz →d xy	0.18
	b 1 B	d xz →d z 2	0.56	2.22 (0.0001)	2.47
		d yz →d xy	0.18
	c 1 B	π a 2 →π * b 1	0.39	2.30 (0.0154)	2.77
		π a 1 →π * b 2	0.34
	c 1 B	π a 2 →π * b 2	0.39	2.31 (0.0118)	2.77
		π a 1 →π * b 1	0.34
	d 1 A	π a 2 →d z 2	0.31	2.61 (0.0000)	3.10
		d yz π a 2 →d z 2 π * b 2	0.19
		d xz π a 2 →d z 2 π * b 1	0.20
	e 1 A	π a 1 →d xy	0.32	2.67 (0.0000)	3.16
		d yz π a 1 →d xy π * b 2	0.12
		d xz π a 1 →d xy π * b 1	0.11

the oscillator strengths and the configurations with weights larger than 0.10, calculated at the RASPT2 level with the 28e26a active space, with values of IPEA shift of 0. and 0.25 a.u. The excited states are labelled in the increasing energy order obtained without IPEA shift.

Table 1 :

 1 RASPT2(28e26a).Continued.The effect of IPEA and the effect of limiting the active space on the porphyrin ring will be discussed in the next subsections. The spectrum of the excited states is rather dense, with 23 excited states whose transition energies range from 1.76 eV to 3.06 eV. The most strongly absorbing states are two nearly degenerated excited states with transition energies of 2.93 eV (f 1 B 1 state) and 2.98 eV (f 1 B 2 state) respectively. They correspond to the second intraporphyrin π → π * absorption band, referred to as the Soret Band in the literature.The second most strongly absorbing states correspond to the first π → π * absorption band (the so-called Q band) at 2.30 eV (c 1 B 2 state) and 2.31 eV (c 1 B 1 state). The absorption intensity of the Q band is around 100 time weaker than that of the Soret Band. The closest available experimental data is the absorption spectrum of carboxyhemoglobin 48 , a protein

whose active site consists in a FeP(im)CO unit (im=imidazole). The strong Soret band has a maximum reported at 2.96 eV, while the Q band has two maxima of nearly same intensity at 2.18 eV and 2.30 eV

48

. Our theoretical results are thus very close to these experimental data, excepting the splitting of the Q band. This splitting could be due to the environmental effect of the protein, which tilts slightly the Fe-CO bond with respect to the porphyrin normal plan

49

. For the closely related FeP(im)CO complex in the gas phase, a TD-DFT study

13

based on the B3LYP functional reports π → π * transitions at 2.40/2.42 eV for the Q band and 3.35/3.36 eV for the Soret band.

The oscillator strengths of the other types of excited states are smaller as can be seen in

Table 1 .

 1 The first MC transition appears at 1.83 eV (a 1 A 2 state) and corresponds to an excitation from d x 2 -y 2 to d xy , both orbitals being oriented in the porphyrin plane. The next MC transitions, at 2.22 eV (b 1 B 1 and b 1 B 2 states) correspond mainly to transitions into the d z 2 orbital which has an iron-CO antibonding character. This finding is thus consistent with the experimental observation of the photolysis of the carbonyl ligand from the heme after irradiation at 570 nm (2.18 eV)5 . The MLCT states, involving excitations from a d orbital to an unoccupied Gouterman π * orbital are located in the lowest part of the spectrum.

  y 2 →π * B d x 2 -y 2 π a 1 →d xy π * B d x 2 -y 2 π a 1 →d xy π *

		b 1	0.68	1.48 (0.0028)	1.99
	a 1 B	d x 2 -y 2 →π * b 2	0.69	1.50 (0.0027)	2.01
	c 1 B	π a 2 →π * b 2	0.50	1.69 (0.0248)	2.69
		π a 1 →π * b 1	0.37
	c 1 B	π a 2 →π * b 1	0.51	1.71 (0.0308)	2.71
		π a 1 →π * b 2	0.37
	b 1 A	d xz →π * b 1	0.42	1.75 (0.7 10 -2 )	2.42
		d yz →π * b 2	0.41
	b 1 A	d yz →π * b 1	0.74	1.93 (0.0000)	2.38
	a 1 A	d x 2 -y 2 →d xy	0.83	1.95 (0.0000)	2.13
	c 1 A	d xz →π * b 2	0.74	1.95 (0.0000)	2.41
	c 1 A	d yz →π * b 2	0.39	1.99 (0.0011)	2.64
		d xz →π * b 1	0.28
	d 1 b 1	0.79	2.29 (0.0001)	3.29
	d 1 b 2	0.80	2.31 (0.0001)	3.30
	b 1 B	d yz →d z 2	0.64	2.36 (0.0001)	2.63
		d xz →d xy	0.22
	b 1 B	d xz →d z 2	0.64	2.36 (0.0001)	2.63
		d yz →d xy	0.22
	e 1 A	π a 1 →d xy	0.21	2.49 (0.0000)	3.69

Table 2 :

 2 B d x 2 -y 2 π a 2 →d xy π * B d x 2 -y 2 π a 2 →d xy π * B d x 2 -y 2 π a 2 →d z 2 π * B d x 2 -y 2 π a 2 →d z 2 π * CASPT2(14e14a). Continued.

			Weights	∆E (eV)	∆E (eV)
				IPEA = 0.0 a.u.	IPEA = 0.25 a.u
	d 1 A	π a 2 →d z 2	0.27	2.50 (0.0000)	3.40
		d yz π a 2 →d z 2 π * b 2	0.26
		d xz π a 2 →d z 2 π * b 1	0.28
	f 1 B	π a 1 →π * b 1	0.48	2.63 (1.2881)	3.78
		π a 2 →π * b 2	0.34
	e 1 b 1	0.80	2.67 (0.0000)	3.58
	f 1 B	π a 1 →π * b 2	0.48	2.68 (1.2982)	3.82
		π a 2 →π * b 1	0.34
	e 1 A	π a 2 →d xy	0.19	2.69 (0.6 10 -6 )	3.65
		d yz π a 2 →d xy π * b 2	0.19
		d xz π a 2 →d xy π * b 1	0.21
	e 1 b 2	0.79	2.71 (0.0000)	3.62
	d 1 A	d x 2 -y 2 →d z 2	0.71	2.88 (0.2 10 -5 )	3.23
	g 1 B	d yz →d xy	0.57	3.19 (0.0001)	3.54
		d xz →d z 2	0.17
	g 1 B	d xz →d xy	0.57	3.21 (0.0008)	3.55
		d yz →d z 2	0.17
	h 1 b 1	0.80	3.33 (0.0103)	4.23
	h 1 b 2	0.80	3.38 (0.0011)	4.27

Table 3 :

 3 2 to 0.4 eV are reported about tests on the N 2 and the benzene molecules. For the other types of states, which involve intraporphyrin excitations or at least depopulation of a porphyrin π orbital, mean values of the increases range from 0.46 to 0.64 eV. Due to the high density of excited states, the introduction of the IPEA shift changes some relative positions of the Transition energies of the excited states corresponding to the Q Band and the Soret Band, obtained from RASPT2 (28e28a active space) and CASPT2 (14e14a active space) calculations with IPEA=0.0 a.u. and IPEA=0.25 a.u.. Experimental results corresponding to the absorption spectra of carboxyhemoglobin is also reported48 .

				∆E (eV)
		RASPT2-28e26a	CASPT2-14e14a	Exp. 48
		IPEA=0.0 a.u. IPEA=0.25 a.u. IPEA=0.0 a.u. IPEA=0.25 a.u
	Q band	2.30	2.77	1.71	2.71	2.18 , 2.30
		2.31	2.77	1.69	2.69
	Soret	2.93	3.57	2.63	3.78	2.96
	band	2.98	3.62	2.68	3.82

different excited states. Some relative orders of the lowest d-d states and the MLCT states are modifed, but in both cases, with or without IPEA shift, the MLCT states lie below the Q absorption band of the porphyrin. Another feature persisting after the introduction of

absorbing Soret band. The extension of the active space on the porphyrin ligand beyond the Gouterman's orbitals is seen to have a strong effect on the states involving intraporphyrin excitations. First, the transition energies of the Q band are significantly improved. Secondly, the effect of inclusion of the IPEA shift on the transition energies is divided by a factor two.

The best agreement with the closest available experimental results on the intraporphyrin excitations is obtained without the inclusion of the IPEA shift and the introduction of the IPEA shift deteriorates this agreement. We conclude from the present work, concerning only singlet valence states, that the IPEA shift should be used carefully and that transitions energies with and without IPEA should be compared.

Configurations Weights ∆E (eV) (Osc. str.)

∆E (eV)


Mo Liu

Anantha Padmanabha

R Ramanujam

Yanjing Wang

Generalized Bundled Fragments for First-Order Modal Logic

Keywords: 2012 ACM Subject Classification Theory of computation → Modal and temporal logics; Theory of computation → Logic bundled fragments, first-order modal logic, decidability, tableaux Digital Object Identifier 10.4230/LIPIcs.MFCS.2022.70

When we bundle quantifiers and modalities together (as in ∃x□, ♢∀x etc.) in first-order modal logic (FOML), we get new logical operators whose combinations produce interesting bundled fragments of FOML. It is well-known that finding decidable fragments of FOML is hard, but existing work shows that certain bundled fragments are decidable [14], without any restriction on the arity of predicates, the number of variables, or the modal scope. In this paper, we explore generalized bundles such as ∀x∀y□, ∀x∃y♢ etc., and map the terrain with regard to decidability, presenting both decidability and undecidability results. In particular, we propose the loosely bundled fragment, which is decidable over increasing domains and encompasses all known decidable bundled fragments.

Introduction

While propositional modal logic (ML) has had extensive applications in system verification and artificial intelligence, and first-order logic (FOL) in finite model theory and database theory, first-order modal logic (FOML) has been studied much less, as it seems to combine the worst of both computationally, leading to undecidability. FOML is a natural specification language for state transition systems where states are given by first-order descriptions of computational domains, with applicability in the realm of database updates, in the control of infinite-state systems, networks with unbounded parallelism and cryptographic protocols. This motivates the study of decidable fragments of FOML. This is a challenge, since even the two-variable fragment of FOML with one unary predicate is undecidable over almost all useful model classes [START_REF] Rybakov | Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter[END_REF]. This situation is to be contrasted against the robust decidability of propositional modal logics ( [START_REF] Vardi | Why is modal logic so robustly decidable?[END_REF][START_REF] Andréka | Modal languages and bounded fragments of predicate logic[END_REF][START_REF] Ganzinger | The two-variable guarded fragment with transitive relations[END_REF]), and the many decidable fragments of first-order logic ( [START_REF] Börger | The classical decision problem[END_REF]).

Despite such discouragement, there have been a few successful attempts: for instance, the monodic restriction, mandating only one free variable in the scope of any modal subformula, yields decidability when combined with a decidable fragment of FOL ( [START_REF] Hodkinson | Decidable fragment of first-order temporal logics[END_REF][START_REF] Wolter | Decidable fragments of first-order modal logics[END_REF]). This idea, arising originally from description logics (cf. [START_REF] Hodkinson | Monodic fragments of first-order temporal logics: 2000-2001[END_REF]) has led to applications in temporal and epistemic logics ( [START_REF] Dixon | Practical first-order temporal reasoning[END_REF], [START_REF] Hodkinson | Decidable and undecidable fragments of first-order branching temporal logics[END_REF], [START_REF] Belardinelli | Quantified epistemic logics for reasoning about knowledge in multi-agent systems[END_REF][START_REF] Belardinelli | Interactions between knowledge and time in a first-order logic for multi-agent systems: Completeness results[END_REF]).

Rather than placing a restriction on variables, or on quantification scope as in the case of guarded fragments [START_REF] Andréka | Modal languages and bounded fragments of predicate logic[END_REF], Wang ([17]) suggested a fragment in which the existential quantifier and the box modality were always bundled together to appear as a single quantifier-modality pair (∃x□). The resulting fragment of FOML enjoys many attractive properties: finite tree model property, PSpace decision procedure and a simple axiom system, without any restriction on predicates or the occurrences of variables. The new operator ∃x□ captures the logical structure of various knowing-wh expressions such as knowing what, knowing how, knowing why, and so on (cf. [START_REF] Wang | Beyond Knowing That: A New Generation of Epistemic Logics[END_REF]), e.g., knowing how to achieve φ can be rendered as there is a plan x such that the agent knows that x can be executed and will guarantee φ.

In [START_REF] Padmanabha | Bundled Fragments of First-Order Modal Logic: (Un)Decidability[END_REF], we took the next step by considering not only the combination ∃x□ but also its companion ∀x□: the logic with both of these combinations continued to be decidable (over increasing domain models). Such modal-quantifier combinations were thus called bundled fragments of FOML. Over models where the domain remains the same in all states, the fragment with both ∃x□ and ∀x□ is undecidable, while the ∃x□-fragment is still decidable.

Clearly, we can define more bundles such as □∀x, □∃x, etc., and indeed further combinations such as ∀x∀y□, and combinations thereof. These (generalized) bundled fragments offer us many interesting possibilities for system specification: ¬∃x□ (x < c): No element is guaranteed to be bounded by constant c (after update).

∃x□ □∃y (x > y):

There is an element that dominates some element after every update. □∃x □∀y (x ≤ y): All updates admit a local minimum.

∃x□ (∃y□ (x > y) ∧ ∃y□ (x < y)):

There is an element that dominates another no matter the update and is dominated by another no matter the update.

Computationally this raises the natural question of what is the most general bundled fragment that is decidable. This is the project taken up in this paper. We consider all possible combinations of the bundled formulas and classify their decidability status. The classification is described in Table 1. We provide a trichotomy: decidable fragments, undecidable fragments and fragments that do not have a finite model property (but where decidability is open).

Towards proving the trichotomy, we first define the notion of loosely bundled fragment which subsumes many decidable bundled fragments of FOML and prove its decidability via a tableau method. We also prove the decidability of another combination of bundled operators where we allow only formulas of the form ∀x□ + □∀x + □∃x (but is not included in the loosely bundled fragment). This requires us to introduce a new proof technique that helps us switch quantifiers in a specific context.

Due to space restrictions, we present only the main ideas and proof techniques of the decidable fragments over increasing domain models in the paper. The proof details, as well as undecidability and lack of finite model property for the other fragments can be found in the detailed technical report in the arXiv [START_REF] Liu | Are bundles good deals for FOML?[END_REF].

Table 1 Satisfiability problem classification for combinations of bundled fragments over increasing domain models. A " * " means no matter the corresponding bundle is included or not.

∀□ ∃□ □∀ □∃

Decidability

✓ ✗ ✗ ✗ ✗ ✓ ✗ ✗ ✗ ✗ ✓ ✗ Subsumed by the ✗ ✗ ✗ ✓ Loosely Bundled Fragment ✓ ✓ ✗ ✗ ✗ ✗ ✓ ✓ * ✓ ✓ * Undecidable ✗ ✓ ✗ ✓ No Finite Model Property ✓ ✓ ✗ ✓ Undecidable ✓ ✗ ✓ ✓ ExpSpace
Loosely Bundled Fragment ExpSpace

Syntax and Semantics

The syntax of first-order modal logic is given by extending the first-order logic with modal operators. Note that we exclude equality, constants and function symbols from the syntax.

▶ Definition 1 (FOML syntax). Given a countable set of predicates P and a countable set of variables Var, the syntax of FOML is given by:

α ::= P (x 1 , . . . , x n ) | ¬α | α ∧ α | ∃xα | □α
where P ∈ P has arity n and x, x 1 , . . . , x n ∈ Var.

The boolean connectives ∨, →, ↔, and the modal operator ♢ which is the dual of □, and the quantifier ∀ are all defined in the standard way. The notion of free variables, denoted by FV(α) is similar to what we have for first-order logic with FV(□α) = FV(α). We write α(x) to mean that x occurs as a free variable of α. Also, α[y/x] denotes the formula obtained from α by replacing every free occurrence of x by y. The monotonicity condition requiring δ(w) ⊆ δ(v) for (w, v) ∈ R is required for evaluating the free variables present in the formula [START_REF] Hughes | A New Introduction to Modal Logic[END_REF]. Because of this, the models are called increasing domain models.

▶
For a given model M we denote W M , R M etc to indicate the corresponding components. We simply use W, R, δ etc when M is clear from the context.

To evaluate formulas, we need an assignment function for variables. For a given model M, an assignment function σ : Var → D is relevant at w ∈ W if σ(x) ∈ δ(w) for all x ∈ Var.

▶ Definition 3 (FOML semantics). Given an FOML model M = (W, D, δ, R, ρ) and w ∈ W, and σ relevant at w, for all FOML formulas α define M, w, σ |= α inductively as follows:

M, w, σ |= P (x1, . . . , xn) ⇔ (σ(x1), . . . , σ(xn)) ∈ ρ(w, P ) M, w, σ |= ¬α ⇔ M, w, σ ̸ |= α M, w, σ |= α ∧ β ⇔ M, w, σ |= α and M, w, σ |= β M, w, σ |= ∃xα ⇔ there is some d ∈ δ(w) such that M, w, σ [x →d] |= α M, w, σ |= □α ⇔ for every u ∈ W if (w, u) ∈ R then M, u, σ |= α We sometimes write M, w |= α(a) to mean M, w, [x → a] |= α(x).
A formula α is satisfiable if there is some FOML structure M and w ∈ W and some assignment σ relevant at w such that M, w, σ |= α. In the sequel, we will only talk about the relevant σ for a given pointed model. Also, while evaluating α, it is enough to consider σ to be a partial function that gives an interpretation for the free variables of α. A formula α is valid if ¬α is not satisfiable.

Bundled fragments

The motivation for "bundling" is to restrict the occurrences of quantifiers using modalities. For instance, allowing only formulas of the form ∀x□α is one such bundling. We could also have ♢∃yα. Thus, there are many ways to "bundle" the quantifiers and modalities. We call these the "bundled operators/modalities". The following syntax defines all possible bundled operators of one quantifier and one modality:

▶ Definition 4 (Bundled-FOML syntax). The bundled fragment of FOML is the set of all formulas constructed by the following syntax:

α ::= P (x1, . . . , xn) | ¬α | α ∧ α | □α | ∃x□α | ∀x□α | □∃xα | □∀xα
where P ∈ P has arity n and x, x 1 , . . . , x n ∈ Var.

Note that the duals of the bundled operators give us the formulas of the form ∀x♢α, ∃x♢α, ♢∀xα, ♢∃xα. Also, note that □α can be defined using any one of the bundled operators where the quantifier is applied to a variable that does not occur in α. However, we retain □α in the syntax for technical convenience.

The following constant domain models may help to get familiar with bundles.

w 1 / / ) ) v 1 : P a w 2 / / ) ) v 2 : P c w 3 / / v 3 : P c u 1 : P b u 2 M 1 M 2 M 3 Let D M1 = {a, b}, D M2 = D M3 = {c}.
□∃xP x holds at w 1 and w 3 but not at w 2 ; ∃x□P x holds only at w 3 ; ¬∀x□P x holds at w 1 and w 2 ; ¬□∀x¬P x holds at all the w i .

We denote ∀□-fragment to be the language that allows only atomic formulas, negation, conjunction, □α and ∀x□α (dually ∃x♢α) formulas, similarly for ∃□-fragment and so on. In general, these fragments are not equally expressive, e.g., as shown by [START_REF] Wang | A new modal framework for epistemic logic[END_REF], the ∃□-fragment cannot express □∃, ∀□ and □∀ bundles over models with increasing (or constant) domains.

In [START_REF] Padmanabha | Bundled Fragments of First-Order Modal Logic: (Un)Decidability[END_REF][START_REF] Liu | On the decision problems of some bundled fragments of first-order modal logic[END_REF] we proved that the ∀□+∃□ and □∀+□∃ fragments are decidable over increasing domain models, while ∀□-fragment and □∀-fragment are undecidable over constant domain models. Since simple bundles become undecidable over constant domain models, in this paper we focus on generalized bundles over increasing domain models.

Note that we can have more general bundled operators of the form ∀x∀y□α etc. This naturally raises the question of what is the most general fragment of this form that is decidable. Towards this, we define a general fragment that subsumes all known decidable bundled fragments so far.

The Loosely Bundled Fragment

Note that a bundled formula of the form ∃x□α imposes a restriction that there is exactly one modal formula in the scope of ∃x. But this is a strong requirement. We weaken this condition to allow formulas of the form ∃xβ where β is a boolean combination of atomic formulas and modal formulas. Moreover, we can allow a quantifier alternation of the form

∃x 1 • • • ∃x n ∀y 1 • • • ∀y m β.
As we will see, the fact that the existential quantifiers are outside the scope of universal quantifiers can help us to obtain decidability results over increasing domain models.

▶ Definition 5 (LBF syntax). The loosely bundled fragment of FOML is the set of all formulas constructed by the following syntax:

ψ ::=P (z 1 , . . . z n ) | ¬P (z 1 , . . . z n ) | ψ ∧ ψ | ψ ∨ ψ | □α | ♢α α ::=ψ | α ∧ α | α ∨ α | ∃x 1 . . . ∃x k ∀y 1 . . . ∀y l ψ
where k, l, n ≥ 0 and P ∈ P has arity n and x 1 , . . . x k , y 1 , . . . y l , z 1 , . . . , z n ∈ Var.

Let LBF be the set of all formulas that can be obtained from the grammar of α above. Note that the syntax does not allow a quantifier alternation of the form ∀x∃y α. Also, inside the scope of quantifier prefix ∃ * ∀ * , we can only have boolean combinations of atomic and modal formulas. The ∃ * ∀ * fragment in FO, (Bernays-Schönfinkel-Ramsey class) has a similar quantifier prefix structure but is different in spirit since there is no modality.

The loosely bundled fragment subsumes some of the combinations of bundled fragments. Hence proving the decidability for LBF implies the decidability for these combinations as well.

▶ Proposition 6. The fragments ∀□ + ∃□ and □∀ + □∃ are subfragments of LBF.

Note that many combinations of bundled operators (for instance □∀ + ∃□) do not form a subfragment of LBF.

Tableau Procedure

Note that the formulas of LBF are in negation normal form (where ¬ appears only in front of atomic formulas). We first define some useful terms and notations.

▶ Definition 7. For any FOML formula φ: φ is a literal if φ is of the form P (x 1 , . . . x n ) or of the form ¬P (x 1 , . . . x n ) φ is a module if φ is a literal or φ is of the form ∆α where ∆ ∈ {□, ♢} The component of φ is defined inductively as follows: If φ is a module then C(φ) = {φ} If φ is of the form φ 1 ∧ φ 2 or φ 1 ∨ φ 2 then C(φ) = C(φ 1 ) ∪ C(φ 2 ) If φ is of the form ∀x φ 1 or ∃x φ 1 then C(φ) = {φ} ∪ C(φ 1 ) A formula φ is called Existential-safe if every ψ ∈ C(φ) is a module or of the form ∀x ψ ′ . A finite set of formulas Γ is Existential-safe if every φ ∈ Γ is Existential-safe.
Intuitively, C(φ) is the set of all subformulas of φ that are "to be evaluated" at the current world. An Existential-safe formula φ does not need any witness from the current local domain in order to make the formula true. The notions of components and existential-safeness will play a role in the tableau-based decision procedure to be introduced below.

Before going into the specific tableau rules, we first explain the general method. A tableau is a tree-like structure generated from a single formula α by repeatedly applying a few rules with some auxiliary information as the root of the tree. Intuitively, a tableau for α is a pseudo model which can be transformed into a real model of α under some simple consistency conditions. We can then decide the satisfiability of a formula by trying to find a proper tableau. As in [START_REF] Wang | A new modal framework for epistemic logic[END_REF], a tableau T in our setting is a tree structure such that each node is a triple (w, Γ, σ) where w is a symbol or a finite sequence of symbols intended as the name of a possible world in the real model, Γ is a finite set of FOML-formulas, and σ is an assignment function for variables. Since we intend to use the set of variables as the domain in the tableau-induced real model, σ is simply a partial identity function on Var, i.e., σ(x) = x for all x ∈ Dom(σ) ⊆ Var, where the domain of σ, Dom(σ), is intended to be the local domain of the real model. The intended meaning of the node (w, Γ, σ) is that all the formulas in Γ are satisfied on w with the assignment σ, thus we also write (w : Γ, σ) for the triple.

A tableau rule specifies how the node in the premise of the rule is transformed to or connected with one or more new nodes given by the conclusion of the rule. Applying the rules can generate a tree-like structure, a tableau, which is saturated if every leaf node contains only literals. For any formula α, we refer to a saturated tableau of α simply as a tableau of α. Further, a saturated tableau is open if in every node (w : Γ, σ) of the tableau, Γ does not contain both β and ¬β for any formula β. 2We call a formula clean if no variable occurs both bound and free in it and every use of a quantifier quantifies a distinct variable. A finite set of formulas Γ is clean if Γ, the conjunction of all formulas in Γ, is clean. Note that every FOML-formula can be rewritten into an equivalent clean formula. For instance, the formulas ∃x□P x∨∀x♢Qx and P x∧□∃xQx are not clean, whereas ∃x□P x ∨ ∀y♢Qy and P x ∧ □∃yQy are their clean equivalents respectively. Clean formulas help in handling the witnesses for existential formulas in the tableau in a syntactic way.

Consider a finite set of formulas Γ that is clean. Suppose we want to expand Γ to Γ ∪ {α 1 , . . . α k }, then even if each of α i is clean, it is possible that a bound variable of α i also occurs in some φ ∈ Γ or another α j . To avoid this, first, we rewrite the bound variables in each α i one by one by using the fresh variables that do not occur in Γ and other previously rewritten α j .

Such a rewriting can be fixed by always using the first fresh variable in a fixed enumeration of all the variables. When Γ and {α 1 , . . . α k } are clear from the context, we denote α * i to be such a fixed rewriting of α i into a clean formula. It is not hard to see that the resulting finite set Γ ∪ {α * 1 , . . . α * k } is clean.

Tableaux for LBF

The tableau rules for the LBF fragment are described in Fig. 1. The (∧) and (∨) rules are standard, where we make a non-deterministic choice of one of the branches for (∨). The rule (END) says that if we are left with only modules and there are no ♢ formulas, then the branch does not need to be explored further. The (♢) rule creates one successor world for every ♢ formula at the current node and includes all the □ formulas that need to be

w : φ1 ∨ φ2, Γ, σ w : φ1, Γ, σ || w : φ2, Γ, σ (∨) w : φ1 ∧ φ2, Γ, σ w : φ1, φ2, Γ, σ (∧) w : ∃xφ, Γ, σ w : φ, Γ, σ ′ (∃) where σ ′ = σ ∪ {(x, x)} w : ∀yφ, Γ, σ w : {φ * [z/y] | z ∈ Dom(σ)}, Γ, σ (∀)
where satisfied along with the ♢ formula and σ is inherited in the successor worlds to preserve the increasing domain property. The (∃) rule picks x itself as the witness to satisfy ∃xφ and (∀) rule expands the set of formulas to include a clean version of φ[z/y] for every variable z in the current local domain.

Note that only the (♢) rule can change (the name of) the possible world, thus creating a new successor. It simply extends the name w by new symbols v i for each successor. Therefore there can be many nodes in the tableau sharing the same world name but such nodes form a path. Given w we use t w to denote the last node sharing the first component w. Given a node t = (w : Γ, σ) in a tableau, we use Dom(t) to denote the domain of σ.

Also, there is an implicit ordering on how the rules are applied: (♢) rule can be applied at a node (w, Γ, σ) only if all formulas of Γ are modules and hence may be applied only after the (∧, ∨, ∀, ∃) rules have been applied as many times as necessary at w. Similarly (∀) rule can be applied only when Γ is Existential-safe which means that the (∃) rule cannot be applied anymore at the current node.

▶ Proposition 8. For every tableau T and every node v = (w, Γ, σ) in T , if v is a leaf then either Γ contains only literals or there is some rule that can be applied at v.

The proposition is true since the LBF ensures that if Γ is not Existential-safe and the (∧, ∨, ♢, END) rules cannot be applied, then it has to be the case that there is some ∃xφ ∈ Γ, for which we can apply the (∃) rule.

▶ Theorem 9. For any clean LBF formula θ, let σ r be an identity mapping over FV(θ) ∪ {z} where z does not occur in θ.

There is an open tableau T with root (r : {θ}, σ r ) iff θ is satisfiable in an increasing domain model.

Proof. First, we claim that the rules preserve the cleanliness of the formulas. To see this, we verify that for every rule, if Γ in the antecedent of the rule is clean, then the Γ ′ obtained after the application of the rules is also clean. This is obvious for (∧), (∨), (♢) and (END) rules. The (∃) rule preserves cleanliness because it frees variable x which is not bound by any other quantifier in the antecedent. The (∀) rule preserves cleanliness by rewriting. Claim. For every node (w : Γ, σ) in T and for every

LBF formula φ, if φ ∈ Γ then M, w, σ |= φ.
The claim is proved using a standard argument by induction on the height of the nodes of T from the leaves to the root (details in [START_REF] Liu | Are bundles good deals for FOML?[END_REF]). Thus, from the claim it follows that M, r, σ r |= θ since the label of the root of T is (r : {θ}, σ r ).

(⇐) From Proposition 8 it follows that we can always apply some rule until every leaf node (w : Γ, σ) is such that Γ contains only literals. Thus every (partial) tableau can be extended to a saturated tableau. To prove that such a tableau is open, it suffices to show that all rules preserve satisfiability (details in [START_REF] Liu | Are bundles good deals for FOML?[END_REF]). ◀

Note that the depth of the tableau is linear in the size of the formula. However, as we have to rewrite formulas using new variables when applying (∀) rule, the size of the domain is exponential in the size of the formula. Hence, the tableau procedure can be implemented in ExpSpace. ▶ Corollary 10. LBF is decidable in ExpSpace.

4

The (Un)decidability Border

Note that the fragment LBF cannot express formulas of the form ∀x∃y□ α and also ∀x□∀y□∀zα. There are many combinations of the bundled fragments that can express thesse formulas (like ∃□ + □∀ and ∀□ + ∃□ + □∃ fragments). In fact, we can prove that a bundled fragment is undecidable if we can assert both ∀x∃y□α and ∀x□∀y□∀z α in the fragment.

To prove this, we can use tiling encoding where ∀x∃y□α can be used to assert that every "grid point" x has a horizontal/vertical successor y. In this case, it is important that both quantifiers are applicable over the same local domain and □α in ∀x∃y□α ensures that the witness y acts uniformly across all the descendants. The second formula ∀x□∀y□∀z α is used to verify the "diagonal property" of the grid. In the companion technical report of this paper [START_REF] Liu | Are bundles good deals for FOML?[END_REF] we prove these results formally. Also, note that there are fragments like ∃□ + □∃ where ∀x∃y□α is expressible but not ∀x□∀y□∀z α. In these cases, we can prove that such fragments do not have a finite model property. This is also proved in the companion technical report [START_REF] Liu | Are bundles good deals for FOML?[END_REF] where we show that this fragment gives a formula that can induce a linear order on the local domain of some world in the model and assert that this linear order does not have a maximal element. This leaves us with the fragments that cannot express ∀x∃y□α formulas and LBF is one such fragment which we proved to be decidable. The fragments ∀□ + ∃□ and □∀ + □∃ also fall in this category and since they are subfragments of LBF, decidability follows. So we only need to consider the fragment ∀□ + ∃□ + □∀ to complete the terrain (cf. Table .

1). The ∀□ + □∀ + □∃ Fragment

In this fragment, we are allowed to express ∀x□α, □∀xα and □∃xα and their duals. Note that this fragment is not closed under subformulas. For instance, φ := ∀x ∃y♢α ∨ ∀z□β is a subformula of φ ′ := ♢∀x ∃y♢α ∨ ∀z□β . But φ ′ is in the fragment and φ is not in the fragment. We say that φ is a subformula of ∀□ + □∀ + □∃ if there is some formula φ ′ ∈ ∀□ + □∀ + □∃ such that φ is a subformula of φ ′ .

Note that even though we cannot express formulas of the form ∀x∃y□φ in the fragment, ∀x∃y♢φ is still allowed. For instance, the formula ♢∀x ∃y♢α is in the fragment. Thus, we can have ∀x∃y♢φ but not ∀x∃y□φ. Intuitively this means that the different witnesses y for each x can work on different successor worlds. The fragment cannot enforce the interaction between x and y at all successors. This property can be used to prove that we can reuse the witnesses by creating new successor subtrees as required.

To get the decidability for ∀□ + □∀ + □∃ fragment, the main idea is to prove that the formulas of the form ∀x∃y♢φ can be satisfied by picking some boundedly many witnesses y that will work for all x. This is the same as proving that if ∀x∃y♢φ is satisfiable then ∃y 1 , . . . ∃y l ∀x ♢φ[y/y i ] is satisfiable (where l is bounded). We illustrate the proof idea with an example. ▶ Example 11. Consider the formula α := ∀x □¬P xx ∧ ∃y♢P xy which is a subformula of the fragment. Let T , r |= α where T is a tree model rooted at r. Now we will modify T to obtain M which is also a tree model rooted at r such that M, r |= ∃y

1 ∃y 2 ∀x □¬P xx ∧ ♢P xy 1 ∨ ♢P xy 2 .
The model M is obtained by extending T in the following way. Let δ T (r) = D r . To obtain M, first we extend the local domain of r by adding a fresh element a. The idea is that for every d ∈ D r (when assigned to x) we will ensure that the new element a can be picked as the y-witness. To achieve this, we do the following: For every d ∈ D r let d ′ ∈ D r and (r, s d ) ∈ R T such that T , s d |= P dd ′ . Let T d be the subtree of T rooted at s d . We will create a new copy of T d and call its root u d . Now, in the new subtree rooted at u d , we make the new element a "behave" like d ′ and we add an edge from r to u d . So, in particular, M will have (r, u d ) ∈ R M such that M, u d |= P da. Since we do this construction for every d ∈ D r we obtain that for all d ∈ D r we have M, r |= ♢P da. Now note that while evaluating α at (M, r) the ∀x quantification will now also apply to a (since a is added to the local domain at r in M). But then, we cannot use a itself as the witness for a since we also need to ensure that M, r |= ∀x□¬P xx. Hence we will add another element b that acts as a witness for a. Further, b also needs a witness. But now we can choose a to be the witness for b since that does not violate the formula ∀x□¬P xx.

So to complete the construction, we pick some arbitrary d ∈ D r for which we have some d ′ ∈ D r and (r, s d ) ∈ R T such that T , s d |= P dd ′ . We create two copies of T d (subtree rooted at s d ) and call their roots as v d and w d respectively. In the subtree rooted at v d we ensure that a and b "behave" like d, d ′ respectively and in the subtree rooted at w d we ensure that a and b "behave" like d ′ , d respectively. In particular, we have M, v d |= P ab and M, w d |= P ba. Finally we add edges from r to v d and from r to w d in M. Note that in principle, it is possible for an ∃ quantified formula to occur in the scope of a ∀ quantifier as a boolean combination with other ∃ quantified formulas and modules. Moreover, these additional formulas can assert some "type" information that may force us to pick additional witnesses. For example, if the formula is ∀x □(¬P xx∧Rx)∨□(¬P xx∧¬Rx) ∧∃y♢ Rx → (P xy ∧¬Ry) ∧ ¬Rx → (P xy ∧Ry) then we need two initial y-witnesses a 1 , a 2 where one is used for witness whose "type" is □(¬P yy ∧ Ry) and other for witness whose "type" is □(¬P yy ∧ ¬Ry) and we also need the corresponding additional witnesses b 1 , b 2 . In general, the formula can force us to pick witnesses of a particular "1-type" which means we might need exponentially many witnesses.

Thus, we need to replace one ∃ inside the scope of ∀ by 2l many ∃ quantifiers outside the scope of ∀ where l is bounded exponentially in the size of the given formulas. We now prove this formally.

For any formula φ if α ∈ C(φ) we denote this by φ[α]. This means that α does not occur inside the scope of any modality in φ. Further, for every α ∈ C(φ) and a formula β, we denote φ[β/α] obtained by rewriting φ where every occurrence of α in φ is replaced by β.

In particular, we are interested in the case where α is of the form ∃y♢ψ. Thus we always consider φ [∃y♢ψ].

For every l ≥ 0 if y = y 1 , y Note that the ∃y quantifier is pulled outside the scope of the ∀x quantifier and replaced with a bounded number of witnesses y 1 , y ′ 1 , y ′ 2 , y ′ 2 . . . y l , y ′ l . Consequently ♢ ψ is replaced with a disjunction each replacing y with one of y i or y ′ i for every i ≤ l. To prove the lemma first we formally define the tree editing operation described in the example. Given a tree model T rooted at r, let d ̸ ∈ D T . To add the new domain element d to a local domain of r, we also need to specify the "type" of the new element d at r and its descendants. Towards this, we pick some domain element c that is already present in δ(r) and assign the type of d to the type of c at every world.

Conclusion

In this paper, we have studied the decidability of bundled fragments of FOML, where we have no restrictions on the use of variables or arity of relations. Specifically, we proved the decidability of the loosely bundled fragment LBF and the ∀□ + □∀ + □∃ fragment. The decidability of these fragments hinges on the observation that ∀x∃y□α is not expressible. A NexpTime lower bound follows for ∀□ + ∃□ and □∀ + □∃ (via encoding the corresponding version of the tiling problem [START_REF] Liu | Are bundles good deals for FOML?[END_REF]), which implies the same lower bound for LBF and ∀□ + □∀ + □∃. There is a significant gap between the upper and lower complexity bounds and we need sharper technical tools for investigating lower bounds for bundled fragments. Note that the quantifier prefix in LBF is of the form ∃ * ∀ * and hence any extension of this quantifier prefix or extending LBF with negation closure will result in a fragment that will be able to express ∀x∃y□ α (and hence will not have the finite model property, [START_REF] Liu | Are bundles good deals for FOML?[END_REF]). In this sense, LBF is the largest fragment in which ∀x∃y□α is not (syntactically) expressible. For the fragment ∀□ + □∀ + □∃ we introduced a technique to pull out ∃ quantifiers outside the immediate scope of ∀ and obtain a finite model property. This technique may be useful in studying other fragments of first-order modal logic.

The results in the paper, along with those in [START_REF] Liu | Are bundles good deals for FOML?[END_REF], provide a trichotomy classification of combinations of bundled operators over increasing domain models (Table 1). The fragments in which we can express both ∀x∃y□α and ∀x□∀y□∀zβ are undecidable, fragments in which we can express the former but not the latter lack finite model property (but decidability is open) and fragments where we cannot express the former are decidable. Similar trichotomy can also be proved for satisfiability over constant domain models [START_REF] Liu | Are bundles good deals for FOML?[END_REF].

We have considered only the "pure" fragments, without constants, function symbols, or equality. The addition of constants is by itself simple, but equality complicates things considerably. Since equality is extensively used in specifications, mapping fragments with equality is an important direction. The study of bundles over models with various frame conditions is also relevant for applications. Unfortunately, while it is clear that equivalence frames lead to undecidability [START_REF] Wang | A new modal framework for epistemic logic[END_REF], even with transitive frames the situation is unclear. Obtaining good decidable fragments over linear frames is an important challenge.

In the context of verification of infinite-state systems, we are often more interested in the model checking problem than in satisfiability. If the domain is finite, the problem is no different from model checking of first-order modal logic. However, we are usually interested in the specification being checked against a finitely specified (potentially infinite) model, e.g., when the domain elements form a regular infinite set. This is a direction to be pursued in the context of bundled fragments.

We have presented tableau-based decision procedures that are easily implementable, but inference systems for reasoning in these logics require further study.

  : Let T be an open tableau rooted at (r : {θ}, σ r ). Define a model M = (W, D, δ, R, ρ) as follows:W = {w | (w : Γ, σ) is a node in T } D = Var R = {(w, v) | v is of the form wv ′ for some v ′ }For every w ∈ W, define δ(w) = Dom(t w ) where t w is the last node of w in T For every w ∈ W and p ∈ P, define ρ(w, P ) = {x | P x ∈ Γ where t w = (w, Γ, σ)}Clearly, M is an increasing domain model, and since z ∈ Dom(σ r ), there is no empty local domain. As T is an open tableau, ρ is well-defined.

  Thus, we have: δ M (r) = δ T (r) ∪ {a, b} and M, r |= ∃y 1 ∃y 2 ∀x □¬P xx ∧ ♢P xy 1 ∨ ♢P xy 2 . With the above construction, this assertion can be verified by assigning y 1 and y 2 to a and b respectively.

▶ Definition 13 .

 13 Given a tree model T = (W, D, R, δ, ρ) rooted at r, let d ̸ ∈ D and c ∈ δ(r). Define the operation of "adding d to δ(r) by mimicking c", denoted by T d →c = (W, D ′ , R, δ ′ , ρ ′ ) where: D ′ = D ∪ {d} for all w ∈ W we have δ ′ (w) = δ(w) ∪ {d}

Definition 2 (FOML structure). An increasing domain model for FOML is

		a tuple M =
	(W, D, δ, R, ρ) where W is a non-empty countable set called worlds; 1 D is a non-empty
	countable set called domain; R ⊆ (W × W) is the accessibility relation. The map δ : W → 2 D
	assigns to each w ∈ W a non-empty local domain set such that whenever (w, v) ∈ R we
	have δ(w) ⊆ δ(v) and ρ : (W × P) →	2 D n is the valuation function, which specifies the
	n
	interpretation of predicates at every world over the local domain with appropriate arity. The
	model M is said to be a constant domain model if for all w ∈ W we have δ(w) = D.

  Let Γ ′ be a clean finite set of formulas such that every α ∈ Γ is a subformula of ∀□ + □∀ + □∃ whereΓ ′ = Γ ∪ {∀xφ[∃y♢ψ]}. If Γ ∧ ∀xφ[∃y♢ψ] is satisfiable then there exists l ≤ 2 |Γ ′ | such that Γ ∧ ∃y 1 ∃y ′ 1 ∃y 2 ∃y ′ 2 .. . ∃y l ∃y ′

′ 1 . . . y l , y ′ l are fresh variables, we denote y♢ψ to be the formula i≤l ♢ψ[y i /y] ∨ ♢ψ[y ′ i /y] which is a big disjunction where each disjunct replaces y in ψ with one of y i or y ′ i . Further, we denote φ[y♢ψ/∃y♢ψ] as simply φ[y♢ψ]. For instance, for the formula φ := P x ∨ ∃y♢Qxy where ψ := ∃y♢Qxy, for l = 2 and y = y 1 , y ′ 1 , y 2 , y ′ 2 being fresh variables, φ[y♢ψ] is given by: P x ∨ ♢Qxy 1 ∨ ♢Qxy ′ 1 ∨ ♢Qxy 2 ∨ ♢Qxy ′ 2 . The size of a formula, denoted by |φ|, is the number of symbols occurring in φ and for a finite set of formulas Γ, let |Γ| = φ∈Γ |φ|. ▶ Lemma 12. l ∀x φ[y♢ψ] is satisfiable, where y = y 1 , y ′ 1 , . . . y l , y ′ l are fresh variables.

Note that FOML can be translated into two-sorted FOL, and due to the Löwenheim-Skolem theorem for countable languages, every model has an equivalent countable model, cf.[START_REF] Braüner | First-order modal logic[END_REF].M F C S

0 2 2

Refer[START_REF] Wang | A new modal framework for epistemic logic[END_REF] for an illustration of a similar tableau construction.

Funding This work is supported by NSSF grant 19BZX135. Anantha Padmanabha: The author is funded by the French government under management of Agence Nationale de la Recherche as part of the "Investissements d'avenir" program, reference ANR-19-P3IA-0001 (PRAIRIE 3IA Institute).

https://arxiv.org/abs/2202.01581

For every w ∈ W and predicate P define ρ ′ (w, P ) = {e ′ | there is some e ∈ ρ(w, P ) and e ′ is obtained from e by replacing zero or more occurrences of c in e by d}.

Suppose that we want to extend the domain with d = d 1 • • • d n which are fresh. Let ω : d → D ′ where D ′ ⊆ δ T (r) and we want each d i to mimic ω(d i ). Then we denote T ω to be the tree obtained by T d1 →ω(d1) d2 →ω(d2)... dn →ω (dn) .

▶ Proposition 14. Let T = (W, D, R, δ, ρ) be a tree model rooted at r with T d →c being an extended tree where d ̸ ∈ D and c ∈ δ(r). Then for all interpretations σ and for all FOML formulas φ and for all w ∈ W we have:

The proposition holds since there is no equality in the syntax and at every world in the extended model, the new element d "behaves" like c and the old elements "behave" like themselves (details in [START_REF] Liu | Are bundles good deals for FOML?[END_REF]). Now we are ready to prove Lemma 12.

Proof of Lemma 12. Let T be a tree model rooted at r such that T , r, σ |= Γ∧∀xφ[∃y♢ψ].

For every domain element a ∈ δ T (r) define:

Note that Π(r, a) formalizes the notion of "type" of a at the world r. This includes the information of all subformulas that are true at the current world, when a universal variable is instantiated with a. Also, since the size of |C(α)| is at most the size of Γ ′ , the set Π

Let M 0 = T ω be the new tree model rooted at r obtained by adding d 1 , d ′ 1 , . . . , d l , d ′ l to δ T (r) where each d i and d ′ i mimics a i . Now M is obtained by extending M 0 as follows:

where ω 1 and ω 2 are defined as follows:

and w i be the root of T i 1 and T i 2 respectively. Add the edges from r to v i and from r to w i in M. The two copies of subtrees are intended to provide witnesses for ∃y♢ψ for d j and d ′ j respectively. We need the two copies to ensure that ω 1 and ω 2 are well defined in the case when i = j and a j ̸ = b.

We now explain the idea behind the construction. Note that T c 0 rooted at u c is created for every c ∈ δ T (r) such that T , r, σ to be the witness for d i and d j to be the witness for d ′ i . Consequently if s i is the world such that a → s i ∈ R T and T , s i , [xy → a i b] |= ψ then we create two new copies of subtree T i rooted at s i and call it T i 1 and T i 2 . By construction, in particular, the new element d i mimics a i and d ′ j mimics b in T i 1 . Similarly d ′ i mimics a i and d j mimics b in T i 2 . Thus, we can pick d ′ j to be the witness for d i (and consider T i 1 ) and pick d j to be the witness for d ′ i (and consider T i 2 ). Also, it is important to note that for every r → v ∈ R M , if d i mimics c and d ′ i mimics c ′ at v then we will always have Π(r, c) = Π(r, c ′ ) = Λ i = Π(r, a i ). Now it can be verified that M, r, σ |= Γ ∧ ∃y To see why the corollary is true, by Lemma 12 we get some l ≤ 2 |Γ ′ | , and we can pad sufficiently many dummy variables to get a strict equality. This gives us a useful tableau rule which we call (∀∃♢) rule for ∀□ + □∀ + □∃ fragment, described in Fig. 2. The full tableau rules for ∀□ + □∀ + □∃ is given by the tableau rules of LBF (Fig. 1) along with the (∀∃♢)-rule. ▶ Theorem 16. For any clean ∀□ + □∀ + □∃ formula θ, let σ r be an identity mapping over FV(θ) ∪ {z} where z does not occur in θ.

There is an open tableau with (r : {θ}, σ r ) as the root iff θ is satisfiable in an increasing domain model.

The proof follows along the lines of Theorem 9. The only interesting part of the proof is to show that the (∀∃♢) rule preserves satisfiability and this is by Lemma 12(details in [START_REF] Liu | Are bundles good deals for FOML?[END_REF]).

Note that at if we start with a formula of length n then the application of (∀∃♢) rule will blow up the formula to size 2 n . So we have a tableau procedure that can be implemented as an algorithm in ExpSpace.

▶ Corollary 17. The fragment ∀□ + □∀ + □∃ is decidable in ExpSpace.


domain: phys sdv

text:
Sophie Theis

Magali Suzanne

Guillaume Gay

Tyssue: an epithelium simulation library

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.