Stéphane Demri

Raul Fervari

Model-Checking for Ability-Based Logics with Constrained Plans

We investigate the complexity of the model-checking problem for a family of modal logics capturing the notion of "knowing how". We consider the most standard abilitybased knowing how logic, for which we show that modelchecking is PSpace-complete. By contrast, a multi-agent variant based on an uncertainty relation between plans in which uncertainty is encoded by a regular language, is shown to admit a PTime model-checking problem. We extend with budgets the above-mentioned ability-logics, as done for ATLlike logics. We show that for the former logic enriched with budgets, the complexity increases to at least ExpSpacehardness, whereas for the latter, the PTime bound is preserved. Other variant logics are discussed along the paper.

Introduction

Knowing How Logics. The epistemic concept of "knowing how" has received considerable attention lately, as a new way of providing formal foundations to strategic reasoning in AI and automated planning (see e.g., (van Ditmarsch et al. 2015)). Most formalisations for this notion are based on simple combinations of standard knowledge modalities and abilities [START_REF] Herzig | Knowing how to play: uniform choices in logics of agency[END_REF][START_REF] Van Der Hoek | Ignore at your peril -towards a logic for ignorance[END_REF]. However, arguably, such an approach does not lead to a proper characterisation of "knowing how", as discussed in [START_REF] Herzig | Logics of knowledge and action: critical analysis and challenges[END_REF][START_REF] Jamroga | Constructive knowledge: what agents can achieve under imperfect information[END_REF].

In (Wang 2018b), a novel proposal to reason about "knowing how" assertions was introduced. The logic (herein written L kh ) includes a goal-direct knowing how modality Khpp, qq, indicating that "the agent knows how to achieve the goal q, whenever the initial condition p holds". As stated in (Wang 2018b), there is an explicit intention to keep the logical language neat and to introduce simple semantical structures, namely labelled directed graphs. The interpretation of the new modality is ability-based: the formula Khpp, qq holds whenever there is a plan σ (understood as a finite sequence of actions) such that from all the states satisfying p, the execution of σ leads only to states satisfying q; and any partial execution of σ can be extended to a complete execution of σ (known as the strong executability condition, directly inspired from conformant planning [START_REF] Smith | Conformant graphplan[END_REF]). Thus, "knowing how" is given by the abilities described by the graph. The simplicity of the log-ical language is partly reflected by the fact that formulae of the form Khpp, qq are global, no action symbol appears in formulae, a single agent is considered, and no "knowing that" modality is present. A complete axiomatisation is provided in (Wang 2018b) but more importantly, such a work has been a source of inspiration for many others. Some variants include: multiple agents, other classes of plans, or admit "knowing that" operators (see e.g. [START_REF] Fervari | Strategically knowing how[END_REF]Li and Wang 2021b)). Other approaches, related to strategic games and coalitions, have been studied in (Naumov and Tao 2018c;Naumov and Tao 2018a;Naumov and Tao 2018b). Finally, the logic studied in [START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF]) (called herein L U ) is based on a notion of indistinguishability over plans. Arguably, such a proposal provides a more epistemic view of knowing how than other approaches.

Substantial progress has been already done related to philosophical motivations, axiom systems and combinations with other epistemic operators. However, much less contributions exist about the possibility to constraint plans (for instance, by adding budgets), or to perform the modelchecking task (instead of checking theoremhood). These issues are addressed in this paper.

Our Motivations. The need to investigate knowing how logics with constrained plans is advocated in (Li 2017, Ch. 3). This is our first motivation to revisit results about numerical constraints (i.e. budgets) and/or regularity constraints about plans, over this family of logics. Moreover, it is more natural to investigate model-checking instead of the validity/satisfiability problem, not only because it is a standard problem in formal verification, but also because the power of adding constraints is best illustrated there. This is due to the fact that the available plans are part of the input, and a few clever tricks cannot be used anymore, such as guessing simply shaped plans witnessing the truth of a formula, see e.g. the completeness proofs in [START_REF] Li | Knowing what to do: a logical approach to planning ad knowing how[END_REF][START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF]. Also, most of the works are dedicated to Hilbert-style axiomatisation and to the satisfiability problem, and relatively little was done on modelchecking, apart from the works [START_REF] Li | More for free: a dynamic epistemic framework for conformant planning over transition systems[END_REF][START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF]Li and Wang 2021a). Since the semantics of such logics involve complex conditions such as strong executability, PTime upper bounds seemed more difficult to reach than what is known about the minimal modal logic K or alternating-time temporal logic ATL (known to admit a PTime model-checking problem, see e.g. [START_REF] Alur | Alternating-time temporal logic[END_REF]). An additional motivation to study the model-checking problem for ability-based logics rests on consequences for the satisfiability problem. It is known that when a logic has the (bounded) small model property, a decision procedure for checking satisfiability consists in guessing a small model and then perform a model-checking test. This is done in (Li 2017, Th. 3.4.8) to decide the satisfiability status of formulae in an extension of L kh , in which the satisfaction of Kh-formulae requires the satisfaction of constraints for intermediate states. Then, knowing the complexity of the model-checking problem becomes crucial to evaluate the complexity of the satisfiability problem. This is the case in (Areces et al. 2021, Sec. 3.3), where the satisfiability problem for an uncertainty-based knowing how logic is shown in NP by stating that model-checking is in PTime.

Our Contributions. We study the model-checking problem for known ability-based logics from the literature, typically from [START_REF] Wang | A logic of knowing how[END_REF] and (Li 2017, Ch. 3), but also for extensions by adding arithmetical and/or regular constraints on plans. Furthermore, we provide new relationships of this family of logics with formal languages and automata theory.

As a warm-up, we show that the model-checking problem for the logic of knowing how from [START_REF] Wang | A logic of knowing how[END_REF] (written L kh ) is PSpace-complete (Thm. 1). This untractability result came a bit as a surprise, but witnesses the high expressive power of the Kh-like modalities despite its simplicity. A variant of the logic L kh designed in [START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF] and featuring a notion of indistinguishable plans, has been shown therein to admit a PTime model-checking problem. Here, we assume that each of those indistinguishability classes is specified by a regular language, thus, can be potentially infinite. We prove that the model-checking problem for this extension L U reg can be also solved in PTime, using an algorithm based on reachability checks (Thm. 2).

We extend the logics L kh and L U reg so that actions have costs, and executing a plan requires to stay within a certain budget. Adding budget-like constraints to plans is advocated in (Li and Wang 2017;[START_REF] Cao | Budget-constrained dynamics in multiagent systems[END_REF]. The extensions we propose follow a standard pattern already used in ATL-like logics (see e.g. [START_REF] Alechina | The virtues of idleness: A decidable fragment of resource agent logic[END_REF][START_REF] Alechina | On the complexity of resource-bounded logics[END_REF][START_REF] Bulling | Combining quantitative and qualitative reasoning in concurrent multi-player games[END_REF]), in energy games (see e.g. [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF]) and in general for other transition systems (see e.g. [START_REF] Cao | Budget-constrained dynamics in multiagent systems[END_REF]). We show that the PTime upper bound is preserved if budgets are added to L U reg (written L U reg p‹q, Thm. 3). This is done by taking advantage of algorithms for solving decision problems related to vector addition systems with states (VASS) (see e.g. [START_REF] Karp | Parallel program schemata[END_REF]), restricted to a single counter, and using Bellman-Ford algorithm for weighted directed graphs (see e.g. [START_REF] Cormen | Introduction to Algorithms[END_REF]. By constrast, we show that adding budgets to L kh increases the complexity significantly. The model-checking problem for L kh p‹q (with resources) is ExpSpace-hard (Lemma 7). The subproblem in which the cost of any action does not depend on the state it is triggered, is shown ExpSpace-complete (Thm. 4).

Preliminaries on a Simple Knowing How Logic

We present below the knowing how logic introduced in (Wang 2015; Wang 2018b) (herein written L kh ). Formulae of the form Khpφ, ψq can be read as "when φ is the case, the agent knows how to make ψ true". Since L kh has a central position in this paper, we dedicate a separate section for preliminary definitions, and for its model-checking problem. Notions introduced here, such as LTS, plans and strong executability, will be helpful in forthcoming sections.

Formulae and models. Let Prop be a countably infinite set of propositional symbols. Formulae of the logic L kh are defined by the grammar:

φ ::" p | ␣φ | φ _ φ | Khpφ, φq (p P Prop).
Other Boolean connectives are defined as usual.

In [START_REF] Wang | A logic of knowing how[END_REF]Wang 2018b), formulae are interpreted over labelled transition systems (LTSs): relational models in which each (basic) relation indicates the source and target of a particular type of action the agent can perform. Let Act be a countably infinite set of action symbols. A labelled transition system (LTS) is a tuple S " pS, pR a q aPAct , Vq, where:

• S is a non-empty set of states (called the domain);

• pR a q aPAct is a collection of binary relations on S;

• V : S Ñ 2 Prop is a labelling function.
Given an LTS S and s a state, the pair pS, sq (parentheses usually dropped) is called a pointed LTS. Before defining the satisfaction relation for the logic L kh , we need to introduce the notion of linear plan, that is used all along the paper (for more complex plans, see (Li and Wang 2021b, Def. 18)).

Linear plans. Let Act ˚be the set of finite sequences over Act. Elements of Act ˚are called plans, with ε being the empty plan. Given σ P Act ˚, let |σ| be the length of σ (|ε| def " 0). For 0 ď k ď |σ|, the plan σ k is σ's initial segment up to (and including) the kth position (with σ 0 def " ε). For 0 ă k ď |σ|, the action σrks is the one in σ's kth position.

Let pR a q aPAct be a family of binary relations with each R a Ď S ˆS. Define R ε def " tps, sq | s P Su and, for all σ P Act ˚and a P Act, R σa def " tps, tq P S ˆS | D t 1 P S s.t. ps, t 1 q P R σ and pt 1 , tq P R a u. Take a plan σ P Act ˚: [START_REF] Wang | A logic of knowing how[END_REF]Wang 2018a;Wang 2018b) handle how to express that an agent knows how to achieve ψ given φ, when she has an appropriate plan that allows her to go from any state in which φ holds only to states in which ψ holds. In order to characterise what 'appropriate' means, one can impose restrictions on what qualifies as an adequate plan.

for s P S define R σ psq def " tt P S | ps, tq P R σ u. For all X Ď S and Π Ď Act ˚, define R Π pXq def " Ť sPX,σPΠ R σ psq. Intuitively,
p s p t q q r a a b Figure 1: Example of LTS.
Let pR a q aPAct as before. A plan σ P Act ˚is strongly executable (SE) at s P S iff for all k P r0, |σ| ´1s and t P R σ k psq, we have R σrk`1s ptq ‰ ∅. We define the set SEpσq def " ts P S | σ is SE at su. Interestingly, in the next section we show that for any state s, the set tσ P Act ˚| s P SEpσqu is a regular language.

Satisfaction relation (,). Let S " pS, pR a q aPAct , Vq be an LTS, s P S and φ be a formula of L kh , , is defined as:

S, s , p def ô p P Vpsq, S, s , ␣φ def ô S, s . φ, S, s , φ _ ψ def ô S, s , φ or S, s , ψ, S, s , Khpφ, ψq def ô there exists σ P Act ˚such that (1) φ S Ď SEpσq and (2) R σ p φ S q Ď ψ S ,
with χ S def " ts P S | S, s , χu. If a plan σ P Act ˚satisfies conditions (1) and ( 2) above, we say that σ witnesses the satisfaction of S, s , Khpφ, ψq. In the LTS S of Fig. 1, we have that S, s , Khpp, qq (via the single-action plan a) whereas S, s . Khpp, rq, as the plan ab is not strongly executable at t P p S .

A complete Hilbert-style system for L kh can be found in [START_REF] Wang | A logic of knowing how[END_REF] (see also (Wang 2018b, Sec. 3)). Decidability of the satisfiability problem for L kh is shown in (Li 2017, Ch. 3) (the proof is done for a more general logic), but its complexity characterisation is open, as far as we know.

3 Model-checking Problem for L kh An LTS S " pS, pR a q aPAct , Vq is finite iff S, Act and Prop are finite sets. The model-checking problem for the logic L kh , written MCpL kh q, is defined as follows.

Input: a finite LTS S and a formula φ over Prop, s P S. Question: S, s , φ?

Though the model-checking problem for many modal and temporal logics can be solved in PTime, see e.g. (Blackburn, de Rijke, and Venema 2001; Demri, Goranko, and Lange 2016), below, we show that MCpL kh q is PSpacecomplete, requiring more computational resources. This high complexity was probably not expected from the works in the literature. Indeed, the model-checking problem is either not considered explicitly at all, or shown in PTime for some variant knowing how logics (see e.g. (Li and Wang 2021a;Li and Wang 2021b)) or shown PSpace-hard but for some expressive logic, see e.g. [START_REF] Li | More for free: a dynamic epistemic framework for conformant planning over transition systems[END_REF].

PSpace-completeness of MCpL kh q. To show PSpacehardness, we reduce the nonemptiness problem for intersec-tion of deterministic finite-state automata that is a PSpacecomplete problem, see e.g. [START_REF] Galil | Hierarchies of complete problems[END_REF][START_REF] Kozen | Lower bounds for natural proof systems[END_REF]. Lemma 1. MCpL kh q is PSpace-hard.

Proof. (sketch) Given N P N, for each i P r1, N s, let A i " pQ i , Act, δ i , q i , F i q be a deterministic finite-state automaton accepting the regular language LpA i q Ď Act ˚. We assume that each automaton A i is complete and the sets of locations are disjoint. We define an LTS S " pS, pR a q aPAct , Vq over the set tinit, finu Ď Prop, with S def " Ţ Q i such that S, q 1 , Khpinit, finq iff LpA 1 q X ¨¨¨X LpA N q ‰ ∅ (q 1 is arbitrary), as follows.

• For all q, q 1 P S and a P Act, pq, q 1 q P R a def ô there is i P r1, N s such that q, q 1 P Q i and q a Ý Ñ q 1 P δ i .

• For all i P r1, N s and q P Q i , init P Vpqq def ô q " q i , and fin P Vpqq

def ô q P F i .
MCpL kh q is PSpace-hard, since Khpinit, finq and S are computed in logspace in the size of the input automata.

In order to establish that MCpL kh q is in PSpace, we show a small plan property based on the regular structure of the set of plans witnessing the satisfaction of S, s , Khpφ 1 , φ 2 q. By regularity, we mean that the set of plans can be shown to be a regular language, and we can effectively compute a finite-state automaton accepting the language of witness plans. Hence, though the regularity property is instrumental to prove our PSpace upper bound, we believe it is also interesting for its own sake to understand the expressive power of the modality Kh in L kh . Below, we state a few properties before getting to the PSpace upper bound.

Given an LTS S " pS, pR a q aPAct , Vq, let us characterise the plans σ P Act ˚such that either (non1) φ 1 S Ę SEpσq or (non2) R σ p φ 1 S q Ę φ 2 S . Let A pt1,t2q " pQ, Act, δ, I, F q be the automaton defined as follows.

• Q def " S, I def " tt 1 u, F def " tt 2 u.
• For all t, t 1 P Q and a P Act, t a Ý Ñ t 1 P δ def ô pt, t 1 q P R a . It is worth observing that t 2 P R σ pt 1 q iff σ P LpA pt1,t2q q. So, the plans σ satisfying (non2) are exactly those in ď tLpA pt1,t2q q | t 1 P φ 1 S , t 2 P ␣φ 2 S u, defined from at most | S | 2 languages. We write Āpt1,t2q to denote the powerset automaton built from A pt1,t2q such that Lp Āpt1,t2q q " Act ˚zLpA pt1,t2q q (complement language). Hence, σ satisfies (2) iff it belongs to the language below.

č tLp Āpt1,t2q q | t 1 P φ 1 S , t 2 P ␣φ 2 S u.
The locations of the automaton Āpt1,t2q are subsets of S.

Let us handle now the condition (non1). We have (non1) iff there is t 1 P φ 1 S such that t 1 R SEpσq, i.e. for some k P r0, |σ| ´1s and u P R σ k pt 1 q, R σrk`1s puq " ∅. Equivalently, (non1) iff there are X 1 , X 2 Ď S such that for some k P r0, |σ| ´1s, X 1 " R σ k pt 1 q, X 2 " R σ k`1 pt 1 q and there is u P X 1 such that for no u 1 P X 2 , we have pu, u 1 q P R σrk`1s . This characterisation serves as the basis to define the set tσ | s P SEpσqu for some state s P S. Let A ‹ s " pQ, Act, δ, I, F q be the finite-state automaton defined as follows.

• Q def " PpSq ˆtacc, reju, I def " tptsu, accqu, F def " PpSq taccu ('acc' stands for 'acceptance', 'rej' for 'rejection').

• For all X P PpSq and a P Act, pX, rejq a Ý Ñ pX, rejq P δ.

• For all X, X 1 P PpSq and a P Act, pX, accq a Ý Ñ pX 1 , accq P δ def ô (‹) R a pXq " X 1 and (‹‹) for all t P X, there is t 1 P X 1 such that pt, t 1 q P R a .

• For all X, X 1 P PpSq and a P Act, pX, accq a Ý Ñ pX 1 , rejq P δ def ô (‹) and not (‹‹). Lemma 2. tσ | s P SEpσqu " LpA ‹ s q. Thus, the plan σ satisfies (1) iff it belongs to the language

č tLpA ‹ t q | t P φ 1 S u,
defined from at most | S | languages; moreover, each automaton A ‹ t has at most 2 ¨2| S| locations. In conclusion, the set of plans witnessing S, s , Khpφ 1 , φ 2 q is equal to

Ş tLpA ‹ t q | t P φ 1 S u X Ş tLp Āpt1,t2q q | t 1 P φ 1 S , t 2 P ␣φ 2 S u,
which amounts to build an automaton with at most

2 |S| ¨| S | 2 22¨| S| ¨| S | locations.
As we have provided a way of characterising conditions (1) and ( 2), we can state an interesting property about the plans witnessing the satisfaction of S, s , Khpφ 1 , φ 2 q. This property has been unnoticed so far, as far as we can judge. Corollary 1. Let S be an LTS, s be a state and Khpφ 1 , φ 2 q be a formula. Let L be set of plans witnessing S, s , Khpφ 1 , φ 2 q. Then, L is a regular language and if L ‰ ∅, then it contains a plan of length at most 2 3¨|S| ¨| S | 3 .

We state the key property to get the PSpace upper bound. Lemma 3. Checking whether S, s , Khpp, qq (with p, q P Prop) can be done in polynomial space.

Proof. (sketch) To test whether S, s , Khpp, qq, we check on-the-fly the non-emptiness of the product automaton

Ś tA ‹ t | t P p S u ˆŚt Āpt 1 ,t 2 q | t1 P p S , t2 P ␣q S u.
There are at most | S | `| S | 2 automata and each location from those automata is a subset of S, possibly enriched with a flag either acc or rej. Polynomial space is enough to store two consecutive locations of the product automaton, and its transition relation can be also computed in polynomial space based on the LTS S. Nonemptiness of finite-state automata can be checked in NLogSpace (the number of states of the product automaton is bounded by 2 3¨|S| ¨| S |

3 ). So, we get a NPSpace decision procedure for checking nonemptiness of the product automaton. By Savitch's Theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], we get the PSpace upper bound.

It is time to characterise the complexity of MCpL kh q. Theorem 1. MCpL kh q is PSpace-complete.

PSpace-hardness is a direct consequence of Lemma 1. In order to establish PSpace-easiness, we can design a standard labelling algorithm taking advantage of Lemma 3 (this idea can be adapted to all the logics studied in this paper).

Variant problems. Our approach using formal languages theory provides us with modular and standard tools in order to characterise the complexity of model-checking problems for several ability-based logics. This is the case for instance, of the logic EPDL, known to be PSpace-complete (Li, Yu, and Wang 2017, Th. 4.3), for which our results can be easily adapted. On the other hand, alternative constraints on plans can be considered. For instance, a modality Kh A (parametric on the finite-state automaton A) such that a witness plan must necessarily belong to LpAq. Another option is to consider variant logics from the literature, such as the logic L khm from (Wang 2018b, Sec. 4) and (Li 2017, Ch. 3)). L khm contains a ternary modality Kh m pφ 1 , φ 2 , φ 3 q, and witness plans must satisfy φ 2 all along the traversed paths. It is not difficult to see that we can apply our techniques for all these logics (details are omitted due to lack of space).

Regular Classes in Uncertainty-Based Logics

It is argued in [START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF]) that an epistemic notion of knowing how should be not only based on the given abilities, but also on some notion of indistinguishability/uncertainty between them. Therein, it is also argued that such an approach makes the framework closer to standard epistemic logics (van Ditmarsch et al. 2015). For instance, it makes easier to move to a multi-agent setting.

In the uncertainty-based setting, agents share the same set of affordances (provided by the actual environment, typically an LTS). Still, they have different abilities depending on which of these affordances are available for each of them, and how well they can tell these affordances apart.

In this section, we assume that the indistinguishability classes of plans are specified by regular languages and we prove that the model-checking problem for this extension L U reg is also in PTime.

Uncertainty-Based Knowing How

Let Agt be a finite set of agent symbols. Formulae of the logic L U are defined by the grammar:

φ ::" p | ␣φ | φ _ φ | Kh a pφ, φq (
p P Prop, a P Agt). A formula Kh a pφ, ψq is read as "when φ is the case, the agent a knows how to make ψ true".

Here, each agent's knowledge is not given simply by the abilities described by the LTS. Instead, the models are enriched with an uncertainty relation " a for each agent a, which is an equivalence relation over a non-empty subset Π a Ď Act ˚describing those plans that are indistinguishable from each other, from the agent's perspective. Below, each relation " a is represented by its set of equivalence classes U a (therefore, U a satisfies a few simple properties recalled below). A multi-agent uncertainty-based LTS (LTS U ) is a tuple S " pS, pR a q aPAct , pU a q aPAgt , Vq where pS, pRq aPAct , Vq is an LTS and each U a assigns to the agent a a non-empty collection of pairwise disjoint non-empty sets of plans with: (1) U a ‰ ∅, (2) ∅ R U a , and

(3)

Π 1 , Π 2 P U a with Π 1 ‰ Π 2 implies Π 1 X Π 2 " ∅.
Intuitively, Π a def " Ť ΠPUa Π is the set of plans that the agent a has at her disposal. Similarly, as in classical epistemic logic, " a Ď Π a ˆΠa describes agent a's indistinguishability. This relation is not defined over possible states of affairs, but rather over her available plans.

Again, in this setting we need to define the notion of being a "proper plan". Let S " pS, pR a q aPAct , pU a q aPAgt , Vq be an LTS U . For Π Ď Act ˚and X Y tsu Ď S, we define

R Π def " Ť σPΠ R σ , R Π psq def " Ť σPΠ R σ psq, and R Π pXq def " Ť tPX R Π ptq.
A set of plans Π Ď Act ˚is strongly executable at s P S iff every plan σ P Π is strongly executable at s. Hence, SEpΠq def " Ş σPΠ SEpσq is the set of the states in S where Π is strongly executable.

The notion of satisfiability for Kh a -formulae is defined as:

S, s , Kh a pφ, ψq def ô there exists Π P U a such that (1) φ S Ď SEpΠq and (2) R Π p φ S q Ď ψ S .

Let S be the LTS from Fig. 1, enriched with U a " tta, abuu and U b " ttau, tabuu, for some a, b P Agt. With this setup, the agent a cannot distinguish between the plans a and ab (i.e., she is uncertain about whether these plans lead to the same outcome or not), whereas the agent b considers them different. Thus, S, s , ␣Kh a pp, qq ^Kh b pp, qq.

The satisfiability problem for L U is NP-complete, whereas MCpL U q is in PTime [START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF]. In an instance of MCpL U q, each U a is defined such that Π a is finite. Representing equivalence relations by their indistinguishability classes results handy for designing model-checking algorithms, as we can directly deal with the list of available plans. However, there is a limitation: we only consider a finite set of them. For instance, assuming that Lpa ˚bq Ď Π a , we may wish to express that for all σ ‰ σ 1 P Lpa ˚bq, we have σ " a σ 1 (the action a is silent for the agent a). In a more concrete example, we can consider that an agent a is a server sending connection requests to another server. The indistinguishability class for a is given by aa ‹ , where action a stands for "sending a connection request through a secure channel". Thus, the class establishes that after the first request is sent by agent a, all other requests are ignored. This type of class cannot be handled when U a is a finite set of finite sets of plans. Instead, below, the elements of U a are defined as finite-state automata A such that LpAq is understood as a (possibly infinite) equivalence class. This is a standard way to represent finitely a (potential) infinite set of words.

Generalisation with Regular Equivalence Classes

Strictly speaking, we generalise the problem MCpL U q from [START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF], by requiring elements in U a to be regular languages (instead of finite sets), but defined through finite-state automata. On the logical side, the models for the logic L U reg defined below, are a subclass of the models for L U (because we assume regularity of each equivalence class). Hence, the introduction of the logic L U reg serves at least two purposes: to generalise MCpL U q and to introduce models in which the indistinguishability classes are regular languages, which might seem confusing at first glance.

An LTS U with regular constraints (reg-LTS U ) is a tuple S " pS, pR a q aPAct , pU a q aPAgt , Vq where each U a assigns to agent a a non-empty collection of finite-state automata ∅ ‰ U a " tA 1 , A 2 , . . .u, such that each A P U a defines an equivalence class over a set Π a " Ť APUa LpAq Ď 2 Act ˚;

i.e., for all A j , A k P U a , j ‰ k implies LpA j q X LpA k q"∅.

The clause for Kh a -formulae over reg-LTS U s becomes:

S, s , Kh a pφ, ψq def ô there is A P U a such that (1) φ S Ď SEpLpAqq and (2) R LpAq p φ S q Ď ψ S .

Unlike [START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF], each equivalence class over Π a is defined by a regular language. Interestingly, theoremhood in L U and L U reg coincide (see (Areces et al. 2021, Th. 2)). A reg-LTS U S " pS, pR a q aPAct , pU a q aPAgt , Vq is finite iff S, Act, Prop and the U a 's are finite sets. The modelchecking problem for the logic L U reg , written MCpL U reg q, is defined over finite reg-LTS U .

In [START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF]) it has been shown that the model checking problem for L U can be solved in PTime. However, herein the main difficulty is dealing with automata generating potentially infinite languages, and thus, equivalence classes with infinitely many plans. One can show that the method used in the previous section applies also here, but giving us (roughly) an ExpSpace upper bound. However, as we will show here, this bound is not optimal. We shall use a more fine-tuned approach to handle the conditions related to the modality Kh a . With this at hand, we will show that MCpL U reg q belongs actually to PTime. The semantics of Kh a pφ, ψq requires to find some A P U a , such that LpAq satisfies two conditions. As U a is finite, inspecting its members one by one, poses no difficulties. Again our method relies on characterising all the potential candidates for the satisfiability of a Kh a -formula that fail to be a proper witness. For A P U a , we proceed as follows.

1. Checking condition (2) R LpAq p φ S q Ď ψ S can be handled by checking that LpAq X Ť tLpA pt1,t2q q | t 1 P φ S , t 2 P ␣ψ S u " ∅, with A pt1,t2q defined as in the previous section. By the analysis provided there, and since nonemptiness of the intersection of two finite-state automata can be checked in PTime, we have a PTime procedure for checking (2).

2. Then, we will design a PTime algorithm for checking the strong executability of LpAq at φ S . The algorithm relies on constructing a directed graph as a product between A and S. Then, we proceed by looking for a state t that fails to execute a "productive" action, i.e., an action that leads to a final state of A, and checking whether pq, tq is reachable, for some location q that is accepting in A. For the sake of correctness, we assume that all the locations in A are productive, i.e. for any location, there is a path in A leading to a final location.

Let S " pS, pR a q aPAct , pU a q aPAgt , Vq be a reg-LTS U and A " pQ, Act, δ, I, F q be an automaton. We define a digraph G " pV, Eq such that V def " Q ˆS and for all pq, tq, pq 1 , t 1 q P V , we have pq, tq Ý Ñ pq 1 , t 1 q P E def ô there is some a P Act such that q a Ý Ñ q 1 P δ and pt, t 1 q P R a . G is therefore a (standard) product between A and S. Given s P S, we define the procedure CheckSEpS, s, Aq as follows.

1. For each a P Act, for each t P S such that R a ptq " ∅ and for each q P Q such that δpq, aq ‰ ∅ do: (a) if there is q 0 P I such that there is a path from pq 0 , sq to pq, tq in G, then: return True; 2. return False.

Lemma 4. sR SEpLpAqq iff CheckSEpS, s, Aq returns True. Now it is time to establish the complexity bound.

Theorem 2. MCpL U reg q is in PTime.

Proof. (sketch) PTime is guaranteed if S, s , Kh a pφ, ψq can be checked in PTime. U a contains a linear amount of finite-state automata and we showed that (2) can be checked in PTime. It remains to verify that so is the case for (1). By Lemma 4, (1) holds iff for all s 1 P φ S , CheckSEpS, s 1 , Aq returns False. As | φ S | ď | S | and the for loop ranges over all S, Act and Q, checking (a) is performed Op| S | 2 ¨| Act | ¨| Q |q times, which is polynomial in the size of the instance S, s , Kh a pφ, ψq. Moreover, (a) is an instance of the graph accessibility problem (GAP), known to be NLogSpace-complete, applied on the graph G of quadratic size in the size of S. Thus, (1) can be checked in PTime.

Ability-Based Logics with Budgets

The need to express budget-like constraints about plans has been advocated in (Li 2017, Sec. 3.1) and (Li and Wang 2017). Assuming that actions have costs, the execution of plans requires that the agent stays always within the budget. Adding resource reasoning is a well-known paradigm used in ATL-like logics, see e.g. [START_REF] Alechina | The virtues of idleness: A decidable fragment of resource agent logic[END_REF], in energy games, see e.g. [START_REF] Chatterjee | The cost of exactness in quantitative reachability[END_REF], and in multi-agent systems, see e.g. [START_REF] Cao | Budget-constrained dynamics in multiagent systems[END_REF]. Herein, we study the complexity of adding resource reasoning in the logics L kh and L U reg , respectively. It is particularly interesting to observe is that the worst-case complexity stays within PTime for the extension of L U reg whereas it jumps to at least ExpSpace-hardness for L kh . We provide clues to understand this computational gap.

Given a set of states S and a finite set of actions Act, a weight function is a map wf : S ˆAct Ñ Z r for some rě0; wf ps, aq is understood as the cost of executing the action a at state s. Adding wf to an LTS shall be our standard way to enrich models with action costs. Given a computation λ "

s 0 a1 Ý Ñ s 1 a2 Ý Ñ s 2 ¨¨¨a K Ý Ñ s K , its weight is defined as wf pλq def " Σ K
k"1 wf ps k´1 , a k q (empty computations have zero cost).

p s q q q t q u a : ´1 a : ´1 b : ´5 b : 0 U a " tÝ Ñ a Ý Ñ e b Ý Ñeu U b " tÝ Ñ a Ý Ñe, Ý Ñ a Ý Ñ b Ý Ñeu
Figure 2: A reg-LTS U with budgets (r " 1).

5.1 PTime Upper Bound for Model-checking L U reg p‹q

We write L U reg prq to denote the ability-based logic L U reg augmented with r ě 0 resource types, and L U reg p‹q to denote the version with an arbitrary number of resource types. This is the version used in our model-checking problem.

For r ě 0, the set of L U reg prq formulae is defined below. a pφ, ψq are read as "when φ is the case, the agent a knows how to make ψ true with budget ⃗ b". Models of the logic L U reg prq are of the form S " pS, pR a q aPAct , pU a q aPAgt , wf , Vq, where wf : S ˆAct Ñ Z r is a weight function. A plan σ " a

1 ¨¨¨a K is ⃗ b-compatible at s ( ⃗ b P N r ) def ô for every computation λ " s 0 a1 Ý Ñ s 1 ¨¨¨a K
Ý Ñ s K with s 0 " s, we have for all L P r1, Ks, ⃗ b `wf pλ ďL q ě ⃗ 0 (with

λ ďL def " s 0 a1 Ý Ñ s 1 ¨¨¨a L Ý Ñ s L ). The plan σ is ⃗ b-compatible at a set X Ď S def ô it is ⃗ b-compatible at all s P X. ⃗ b is understood as the initial budget.
Given a model S " pS, pR a q aPAct , pU a q aPAgt , wf , Vq and s P S, we update the satisfiability clause for Kh Consider the model S of Fig. 2 (we use standard notations for finite-state automata). Both plans a and ab lead to q states, but the cost of executing ab from s to u is ´1, whereas from s to t is ´6. Thus, S, s , Kh 5 b pp, qq ^␣Kh 5 a pp, qq. In the budget-free logic L U reg , the clause related to the satisfaction of Kh a pφ, ψq uses exactly (1) and ( 2) above. We have shown that such conditions can be checked in PTime.

To prove that MCpL U reg p‹qq is in PTime too, we establish that (3) can be checked in PTime for a given A. Since | S | is less than the size of S and MCpL U reg p‹qq can be solved by a standard type of labelling algorithm, it is sufficient to show that given S, t P S and a finite-state automaton A, one can check in PTime that for all σ P LpAq, σ is ⃗ b-compatible at t. This is the purpose of the rest of this subsection.

Interestingly, the models for L U reg prq can be viewed as an extension of the vector addition systems with states (VASS) [START_REF] Karp | Parallel program schemata[END_REF], since in both models the transitions are labelled by tuples in Z r encoding an update function. Below, we recall a few standard definitions about VASS that are helpful in the sequel to characterise the complexity of MCpL U reg p‹qq. A vector addition system with states (VASS) is a structure V"pQ, r, Rq, where Q is a finite set of locations, rPN is its dimension, and R is a finite set of transitions in Q ˆZr ˆQ. A configuration (resp. pseudoconfiguration) in a VASS V is a pair pq, ⃗ xq P Q ˆNr (resp. in Q ˆZr ). Given pseudo-configurations pq, ⃗ xq, pq 1 , ⃗ x 1 q and a transition T " q ⃗ u Ý Ñ q 1 , we write pq, ⃗ xq T Ý Ñ pq 1 , ⃗ x 1 q whenever ⃗ x 1 " ⃗ u `⃗ x. A pseudo-run is defined as a sequence ρ " pq 0 , ⃗ x 0 q T1 Ý Ñ pq 1 , ⃗ x 1 q T2 Ý Ñ pq 2 , ⃗ x 2 q ¨¨¨of pseudo-configurations, where pq 0 , ⃗ x 0 q is the initial pseudoconfiguration. A run is a pseudo-run in which only configurations in Q ˆNr occur.

An r-VASS is a VASS with r ě 0 counters. We begin by presenting a simple problem called NONSAFE(VASS), strongly related to the non-satisfaction of the condition (3).

Input: a VASS V and a configuration pq 0 , ⃗ x 0 q P Q ˆNr . Question: is there a finite pseudo-run ρ " pq 0 , ⃗ x 0 q Ý Ñ pq 1 , ⃗ x 1 q Ý Ñ ¨¨¨Ý Ñ pq n , ⃗ x n q such that ⃗ x n R N r ? (is it possible to reach a negative value from pq 0 , ⃗ x 0 q?).

Lemma 5. NONSAFE(VASS) is in PTime.

Lemma 5 follows from the fact that one instance of NONSAFE(VASS) can be reduced to r instances of NONSAFE(1-VASS) (restriction to 1-VASS). The second step consists in showing that checking whether a negative value can be reached in a 1-VASS from a given initial configuration can be solved using Bellman-Ford algorithm working on weighted directed graphs.

Assume that A " pQ, Act, δ, I, F q and all the locations in Q are productive, so any run reaching a given location from some initial location can be completed as an accepting run.

One more step is needed to establish that (3) can be solved in PTime. Namely, we build a VASS V " pQ 1 , r, R 1 q with Q 1 def " S ˆQ such that not (3) iff there is q 0 P I and t P φ S such that V, ppt, q 0 q, ⃗ bq is a positive instance of NONSAFE(VASS). It remains to define R 1 . We have ps, qq ⃗ u Ý Ñ ps 1 , q 1 q P R 1 def ô for some a P Act, ps, s 1 q P R a and q a Ý Ñ q 1 P δ (synchronisation on actions) with ⃗ u " wf ps, aq. Lemma 6. There are t P φ 1 S and σ P LpAq such that for some j P r1, | σ |s, σ j is not ⃗ b-compatible at t iff there are t P φ 1 S and q 0 P I such that V, ppt, q 0 q, ⃗ bq is a positive instance of NONSAFE(VASS). Now, we are in position to state our best result as far as a PTime model-checking problem is concerned. 2) and (3) hold. There is a linear amount of automata in U a and Thm. 2 guarantees that ( 1) and ( 2) can be checked in PTime. The remaining bit is to check that (3) can be done in PTime. Notice that when (1) and ( 2) hold true, the first statement of Lemma 6 is equivalent to (3) being false. Thus, checking (3) follows from the combination of Lemmas 5 and 6.

Extending the Logic L kh with Budgets

Let L kh prq be the ability-based logic L kh augmented with r ě 0 resource types. The logic L kh p‹q denotes the version in which the number of resource types is arbitrary.

Models of L kh prq are of the form S " pS, pR a q aPAct , wf , Vq where wf : S ˆAct Ñ Z r is a weight function. The relation , is updated as follows.

S, s , Kh

⃗ b pφ, ψq def ô there is a plan σ P Act ˚such that (1) and ( 2) as for L kh , and (3) σ is ⃗ b-compatible at φ M .

We already showed that the conditions (1) and ( 2) from L kh can be encoded by a finite-state automaton of exponential size, and that MCpL kh q is PSpace-complete. However, MCpL kh p‹qq witnesses at least an exponential blow-up, as stated below, partly due to condition (3) combined with (2).

Lemma 7. MCpL kh p‹qq is ExpSpace-hard.

The proof is by reduction from the control-state reachability problem for VASS, written CREACH(VASS), known to be ExpSpace-complete, see e.g. [START_REF] Lipton | The reachability problem requires exponential space[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. CREACH(VASS) takes as inputs a VASS V, a configuration pq 0 , ⃗ x 0 q, and a location q f and asks whether there is a run from pq 0 , ⃗ x 0 q to a configuration with location q f . Cor. 1 states that small witness plans in L kh have length at most exponential in the joint size of the LTS and the formula. By contrast, since the proof of Lemma 7 uses a reduction from CREACH(VASS) for which witness runs can be of length doubly-exponential in the size of the input VASS [START_REF] Lipton | The reachability problem requires exponential space[END_REF]), the witness plans in L kh p‹q may have length doubly-exponential too (if not more). Up to now, no known upper bound exists for the length of witness plans in L kh p‹q and the decidability status of MCpL kh p‹qq is open.

However, it is possible to characterise the complexity of a natural fragment of MCpL kh p‹qq by requiring a simple restriction on the weight function in LTS: we consider below the subproblem of MCpL kh p‹qq in which the action costs do not depend on the states the actions are triggered. Hence, to conclude, we assume that wf is of the form Act Ñ Z r . Theorem 4. MCpL kh p‹qq restricted to LTS with action costs independent of states is ExpSpace-complete. For r P N, its restriction to r resources is PSpace-complete.

ExpSpace-hardness is inherited from the proof of Lemma 7. For ExpSpace-easiness, we show that testing S, s , Kh ⃗ b pp, qq can be reduced to an instance of CREACH(VASS) that can be checked in nondeterministic exponential space (refined analysis required here). When r is fixed, we regain PSpace.

Concluding Remarks

We investigated the complexity of the model-checking problem for ability-based logics, possibly with plans constrained by budget-like requirements and/or by regularity constraints. First, we established that for the well-known knowing how logic introduced in (Wang 2015), the problem is PSpacecomplete (Thm. 1). Interestingly, we have shown that the set of witness plans for a given Kh-formula is regular, a property used all along the paper. Then, we propose a generalisation of the uncertainty-based logic of [START_REF] Areces | Uncertainty-based semantics for multiagent knowing how logics[END_REF], in which each equivalence class over sets of plans is defined by a regular language. We show that modelchecking for this extension L U reg is in PTime, using an algorithm based on graph accessibility (Thm. 2). The final part of the paper is devoted to add budget-like constraints to L kh and L U reg , following a paradigm used in many formalisms. While model-checking for the extension L U reg p‹q is shown in PTime (Thm. 3), we prove that for L kh p‹q is ExpSpacehard (Lemma 7). Moreover, the restriction in which the action costs do not depend on states, a reasonable assumption in many contexts, is ExpSpace-complete (Thm. 4). In all cases, we rely on results from vector addition systems.

A puzzling question remains the decidability status of MCpL kh p‹qq. Our investigations can be also broadened by going beyond sequential plans (see e.g. (Li and Wang 2021b)) or by investigating alternative knowing how modalities (see e.g. [START_REF] Fervari | Strategically knowing how[END_REF]).

φ

  ::" p | ␣φ | φ _ φ | Kh ⃗ b a pφ, φq (p P Prop, a P Agt, ⃗ b P N r ) All the integers appearing in formulae and models are encoded with a binary representation. Formulae of the form Kh ⃗ b

ô

  there is A P U a such that (1) φ M Ď SEpLpAqq, (2) R LpAq p φ M q Ď ψ M , and (3) for all σ P LpAq, σ is ⃗ b-compatible at φ M .

Theorem 3 .

 3 MCpL U reg p‹qq is in PTime. Let us briefly provide the argument to get PTime. The proof of Thm. 3 uses a labelling algorithm as for Thm. 1 and PTime is guaranteed as soon as M, s , Kh ⃗ b a pp, qq can be checked in PTime. Now, M, s , Kh ⃗ b a pp, qq there is A P U a such that (1), (

Acknowledgments

We thank the reviewers for their constructive comments and suggestions. Stéphane Demri is supported by Centre National de la Recherche Scientifique. Raul Fervari is supported by ANPCyT-PICT-2020-3780, CONICET PIP 11220200100812CO, and by the Laboratoire International Associé SINFIN.


Electronic Supplementary information

Sup. Figure 1: A small (top) and a large rearrangement event (bottom) that cannot be easily discerned by sight. We provide the images and then the results of the image analysis quantifying each event. In the latter the rearrangement event is in white, taking place within the outlined rectangle in the raw images, while the rest of the accumulation is in grey. The time between each image is 0.01s, the scale bars correspond to 10µm.

Electronic Supplementary Material (ESI) for Soft Matter. This journal is © The Royal Society of Chemistry 2022 Sup. Sup. Table : The composition of the accumulations as a percentage for 2µm PS (left) and 1.8µm PS (right) particles for various salt concentrations.


Emily Öhman
email: ohman@waseda.jp

Riikka Rossi
email: riikka.rossi@helsinki.fi

Affect as a proxy for literary mood

We propose to use affect as a proxy for mood in literary texts. In this study, we explore the differences in computationally detecting tone versus detecting mood. Methodologically we utilize affective word embeddings to look at the affective distribution in different text segments. We also present a simple yet efficient and effective method of enhancing emotion lexicons to take both semantic shift and the domain of the text into account producing real-world congruent results closely matching both contemporary and modern qualitative analyses.

Introduction

In this study, we explore how the literary concept of mood can be studied and detected with computational methods. We propose to use affect as a proxy for mood and test our hypothesis first quantitatively on different segmentations of the different texts, and then qualitatively against expert close-readings of the same texts. We use multiple different natural language processing (NLP) approaches to attempt to identify the origins, construction, and location of mood. For this purpose, we have collected a corpus of nearly 1000 literary works published in Finnish around the year 1900. Our paper utilizes many common NLP methods and approaches from computational literary studies and affective computing, but besides our pilot study [START_REF] Öhman | Computational exploration of the origin of mood in literary texts[END_REF], to our knowledge, it is the first study to combine emotion detection/sentiment analysis with the study of mood in texts.

We focus on mood as it is one of the more ephemeral yet pervasive aspects of a literary text. Mood is typically described as the atmosphere that the author creates through their word choices, style, and use of imagery and can sometimes even include tone. The line between tone and mood can be difficult to draw, particularly when approaching the topic with computational tools, but succinctly the difference can be explained as mood being about how the reader feels about the text, and tone about how the implied author feels about it and uses words to convey their own attitude towards a topic or subject1 [START_REF] Turco | The book of literary terms: the genres of fiction, drama, nonfiction, literary criticism, and scholarship[END_REF].

Although many different literary tools contribute to the creation of mood, perhaps the most important one, that influences all the other tools as well, is the choice of words. Typically in literature, the intentionality of word choice is higher than in most other text genres (e.g. social media posts) [START_REF] Mitchell | Intention and Text: Towards an Intentionality of Literary Form[END_REF][START_REF] Öhman | Xed: A multilingual dataset for sentiment analysis and emotion detection[END_REF]. It is therefore a great subject for analyzing the use and intensity of emotion-associated words in text. As there are so many components that help create mood, in a larger sense mood is not reducible to a single aspect, but generated by a set of textual elements, however, we can use the importance of word choice to our advantage. If we look at the affective distribution of the words in texts using different text segments, we can attempt to pinpoint where in a text mood is created and how that links to affect.

We suggest that the computational study of the valence of the lexicon of a literary text can be valuable in providing an accurate picture of the distribution of the positive and negative valence in a text continuum, and thus help us to better understand the relationship between the linguistic qualities of a text and its perceived emotional effects, particularly the mood of a text. Furthermore, we contribute to the discussion of the most suitable tools for interdisciplinary work including the debate about lexicon-based methods versus machine learning as the most "accurate" [START_REF] Wouter Van Atteveldt | The validity of sentiment analysis: Comparing manual annotation, crowdcoding, dictionary approaches, and machine learning algorithms[END_REF][START_REF] Ohman | The validity of lexicon-based emotion analysis in interdisciplinary research[END_REF][START_REF] Teodorescu | Frustratingly easy sentiment analysis of text streams: Generating high-quality emotion arcs using emotion lexicons[END_REF].

Background & Previous Work

Around the turn of the millennium the "affective turn" took place [START_REF] Greenwald | Postmodernism and the affective turn[END_REF][START_REF] Armstrong | The affective turn in contemporary fiction[END_REF].

It was a shift in attitude regarding the importance of affect in humanities and social science research, including literary studies [START_REF] Kim | The affective turn: Theorizing the social[END_REF]. Literature can be considered a domain where the affective functions of language are of principal importance [START_REF] Colm | What literature teaches us about emotion[END_REF]. The affective turn has led to a significant increase in research that focuses on the affective side of text in literature [START_REF] Armstrong | The affective turn in contemporary fiction[END_REF].

The affective power of literary texts has been acknowledged since Aristotle's Poetics, but in the 20th century, many schools of thought such as formalism, new criticism, structuralism and poststructuralism orientated the attention to formal and structural aspects of texts, whereas the study of emotions was excluded and considered as susceptible to researchers' subjective emotions. Research topics range from the study of literature and empathy [START_REF] Keen | Empathy and the Novel[END_REF] to the study of literature and cognition (Hogan, 2011)), negative affects and tone in texts [START_REF] Ngai | Ugly feelings[END_REF] to empirical perspectives [START_REF] Sklar | The Art of Sympathy in Fiction : Forms of Ethical and Emotional Persuasion[END_REF][START_REF] Van Lissa | Difficult Empathy-The Effect of Narrative Perspective on Readers' Engagement with a First-Person Narrator[END_REF], and even emotions specific to Finnish literature [START_REF] Rossi | Alkukantaisuus ja tunteet -Primitivismi 1900-luvun alun suomalaisessa kirjallisuudessa[END_REF][START_REF] Rossi | Pohjoisia tunteita[END_REF].

Recent studies on emotions in Finnish literature demonstrate that Finnish literature presents us with a rich body of work for developing the general theory of literature and emotions and to study the ways in which genre-specific emotional effects vary culturally and historically [START_REF] Rossi | Pohjoisia tunteita[END_REF]. While this research has opened up new perspectives it has also demonstrated there are a number of gaps and complex questions to resolve. Along with the affective turn, the question of a text's overall emotional tone or mood has aroused vivid interest (e.g. [START_REF] Ngai | Ugly feelings[END_REF], Lyytikäinen (2017), and Rossi (2020)). However, a systematic theory of how tone and mood are created and triggered in the reader is still in the works.

We suggest that a study of the emotional valence of the lexicon measured quantitatively provides a new approach that can help with understanding the components of a text's mood (Öhman andRossi, 2021, 2022). Furthermore, it has been shown that lexicon-based methods can achieve better results in emotion classification tasks than machine learning models, especially when the text segment size is optimized [START_REF] Ohman | The validity of lexicon-based emotion analysis in interdisciplinary research[END_REF][START_REF] Teodorescu | Frustratingly easy sentiment analysis of text streams: Generating high-quality emotion arcs using emotion lexicons[END_REF].

Parallel to the affective turn, sentiment analysis became an active field of research within nat-ural language processing and computer science [START_REF] Mäntylä | The evolution of sentiment analysis-a review of research topics, venues, and top cited papers[END_REF]. Sentiment analysis and emotion detection has been used with literary works with varying levels of success; [START_REF] Kim | A survey on sentiment and emotion analysis for computational literary studies[END_REF] provide a substantive overview of sentiment analysis and emotion detection as it is used in CLS. Although many of the papers cited in the review are interesting and innovative, virtually none of them deal with topics that are common in more traditional literary studies. Common CLS topics are genre classification by emotion, story-type, sentiment tracking, and sentiment recognition (see e.g. [START_REF] Sprugnoli | Towards sentiment analysis for historical texts[END_REF][START_REF] Schmidt | An evaluation of lexicon-based sentiment analysis techniques for the plays of gotthold ephraim lessing[END_REF][START_REF] Amano | An analysis of representative works of japanese l iterature based on emotions and topics[END_REF].

As interesting and innovative as previous CLS work is, it is typically of little use to literary scholars studying affect. These CLS approaches rarely work in harmony with literary analysis in the traditional sense and usually do not even touch upon the topics that interest literary scholars such as tone, mood, and emotion evocation. We hope that our efforts will contribute to merging the talents and knowledge within CLS, digital humanities, NLP, as well as traditional literary studies.

Although there are exceptions (see e.g. [START_REF] Hu | Dynamic evolution of sentiments in never let me go: Insights from multifractal theory and its implications for literary analysis[END_REF][START_REF] J Berenike Herrmann | Linguistic metaphor identification in german[END_REF], it is somewhat rare for studies within the field of CLS to have literary experts working on the project, and many such projects rely heavily on the analysis of the quantitative results conducted by experts of NLP rather than experts of literature. This is not a problem in only CLS, but in many other interdisciplinary fields, particularly those with a computational element [START_REF] Bartlett | The locus of legitimate interpretation in Big Data sciences: Lessons for computational social science from-omic biology and high-energy physics[END_REF]. This is why we think it is imperative to conduct CLS (and other interdisciplinary studies) with domain experts and not just NLP knowledge and literary data. CLS as a field has been criticized for providing either obvious results or ephemeral results that are not robust enough for repeat analysis [START_REF] Da | The computational case against computational literary studies[END_REF]. Furthermore, there seems to be a pervasive belief that state-of-the-art methods from NLP are the most accurate when used on non-standard unstructured data regardless of the research question of the downstream application of such methods [START_REF] Ohman | The validity of lexicon-based emotion analysis in interdisciplinary research[END_REF]. It is commonly suggested that machine learning methods are more accurate than lexiconbased ones (see e.g. [START_REF] Wouter Van Atteveldt | The validity of sentiment analysis: Comparing manual annotation, crowdcoding, dictionary approaches, and machine learning algorithms[END_REF]), but several recent papers have suggested this is not the case, especially when dealing with emotional arcs and ideal bin sizes in verbose domains [START_REF] Ohman | The validity of lexicon-based emotion analysis in interdisciplinary research[END_REF][START_REF] Teodorescu | Frustratingly easy sentiment analysis of text streams: Generating high-quality emotion arcs using emotion lexicons[END_REF]. We have taken the criticism of both camps to heart in an effort to produce robust and reliable but also useful and interpretable results.

Data

Our data collection was simple and straightforward. Although there exists R packages and Python libraries for handling Project Gutenberg downloads, Project Gutenberg discourages mass downloads using such methods, thus we used their recommended method for filtering works using http queries and downloading a set smaller amount of books at a time. We downloaded the first2 1000 books from Project Gutenberg3 , with two filter criteria: (1) the language was Finnish, and ( 2) the text was in utf-8 plain text format. There is currently no method for filtering out translated works so we estimate that the dataset consists of approximately 50% translated texts.

We used the simple gutenberg-cleaner4 to get rid of the preamble and the legal text at the end of the book, then we created a regex to extract key information such as the title, the name of the author, the year of publication, and whether the book was originally written in Finnish. The translation status of the book was extracted based on whether the terms suomentaja, suomennettu, suomentanut, or any version of kääntäjä/käännös/käännetty etc.5 were present within the first ten lines of text after the preamble was removed.

Although we filtered books based on their encoding, a fairly large number of the books were not actually utf-8 encoded and had to be decoded and re-encoded. We used automatic encoding detection and tried to convert the texts to utf-8, but for some works this failed and in the end due to these encoding issues, our final corpus consists of 975 books instead of 1000. A vast majority (95+%) were written or translated between the years 1850 and 1925 and over 90% after 1880, with only a few instances of older texts, which means that the language used in the texts can be considered Modern Finnish [START_REF] Forsman | Virtuaalinen vanha kirjasuomi[END_REF]. The final data consists of 2,938,032 sentences and 41,417,116 tokens.

The Emotion Intensity Lexicon

We used the Finnish Emotion Intensity Lexicon (FEIL) (Öhman, 2022) as a starting point for detecting affective terms. FEIL is based on the NRC emotion lexicon [START_REF] Saif | Crowdsourcing a word-emotion association lexicon[END_REF] and emotion intensity lexicon [START_REF] Saif | Word affect intensities[END_REF] and has been adapted for Finnish. It lists words alongside the emotions they are associated with as well as the intensity of the associated emotion as a number between 0 and 1. The emotions roughly correlate with Plutchik's wheel of emotions [START_REF] Plutchik | A general psychoevolutionary theory of emotion[END_REF] and contains the emotions anger, anticipation, disgust, fear, joy, sadness, and trust. We follow the best practices and ethical guidelines as set forth by Mohammad (2022a,b).

Method

Finnish is a fairly easy language to work with in terms of NLP. There are numerous high-quality resources that are actively maintained and new tools are constantly being developed for various written standards of Finnish and Finnish-adjacent languages. Nearly all of these resources are also open-source and freely available (Hämäläinen and Alnajjar, 2021). Therefore, we were privileged enough to have several different lemmatizers and tokenizers at our disposal, some even specifically made for older Finnish texts. We also added to this list by creating a Finnish version of the chapterize Python package6 package.

Once the data was cleaned, we preprocessed it by lemmatizing, splitting it into paragraphs, and tokenizing the texts. We attempted to fine-tune Finnish BERT [START_REF] Virtanen | Multilingual is not enough: BERT for Finnish[END_REF] to work with our texts (as per [START_REF] Gururangan | DEMix layers: Disentangling domains for modular language modeling[END_REF]), but the vocabulary was not improved sufficiently to work with data so different from the original training data for Finnish BERT. In order to find the best tool for our data we tried multiple different lemmatization tools. These tools included the Turku Neural Parser [START_REF] Kanerva | Universal Lemmatizer: A Sequence to Sequence Model for Lemmatizing Universal Dependencies Treebanks[END_REF], murre [START_REF] Partanen | Dialect text normalization to normative standard Finnish[END_REF]Hämäläinen et al., 2021), and both the experimental and news Finnish spaCy models. In the end we settled for the Turku Neural Parser as the results were the most accurate (see table 1 for an example) and all words were not only parsed but parsed correctly in context as well.

In the example, the Turku Neural Parser was the only one able to correctly parse the nonstandard form kahvians -standard form: kahviansa -partitive case of 3rd. pers. sing./plur. coffee. Incidentally, in the dissertation of [START_REF] Airio | Morphological Problems in IR and CLIR[END_REF] kahviansa is discussed as an example of "parasite words" since it can be mistakenly split into kahvi (coffee) and ansa (trap), something none of the lemmatizers did. With careful optimism, we take this as a demonstration of how good lemmatizers for morphologically complex languages have become in the past decade.

The different lemmatizers had different strengths and weaknesses. For example, spaCy is very easy to use and install, it is reasonably fast for this amount of text, and also produces other information that most of the other lemmatizers leave out. It is therefore great for exploring other aspects of the data such as NER and similarity scores. However, the Turku Neural Parser produced the best results in an easy-to-use pipeline7 . Omorfi [START_REF] Pirinen | Omorfi-free and open source morphological lexical database for finnish[END_REF] and FinPos [START_REF] Silfverberg | Finnpos: an open-source morphological tagging and lemmatization toolkit for finnish[END_REF] might also have been good candidates for lemmatizers, but these proved difficult to install on the platforms available for this project.

Once we had the texts lemmatized and tokenized, we attempted to identify the first three paragraphs of each text. This was a more complex process than expected as even after removing the preambles/headers and footers, miscellaneous metadata of various shape cluttered the start of the book. There was very little uniformity or even commonly recurring patterns of where the actual text of the book or chapters starts. This led us to create a Finnish version of the chapterize package for Python, which enabled use to split texts into chapter and recognize opening paragraphs when used in conjunction with the sentence and paragraph ids provided by the conllu metadata generated by Turku Neural Parser. We used two different text sections as targets for overall mood detection: the first three paragraphs of each book, and the first 200 tokens from each chapter in each book.

The size of the bins was chosen based on findings by [START_REF] Teodorescu | Frustratingly easy sentiment analysis of text streams: Generating high-quality emotion arcs using emotion lexicons[END_REF] that suggest even at a few hundred tokens, lexiconbased methods can excel at estimating emotion arcs beyond current state-of-the-art machine learning capabilities. They suggest that lexicon-based approaches are more suitable "for applications where simple, interpretable, low-cost, and low-carbonfootprint systems are desired" (Teodorescu and Mohammad, 2022, 8).

Previous studies [START_REF] Öhman | The Language of Emotions: Building and Applying Computational Methods for Emotion Detection for English and Beyond[END_REF] have made it clear that although the results from lexiconbased emotion detection can be very accurate in terms of real-world congruency, certain words can easily obfuscate the results. One of the literary works used as quality assessment and proof-ofconcept the novel Rautatie (Railroad) by Juhani Aho focuses on the novelty of a railroad track coming to town and naturally contains many instances of the word railroad, the fact that the word itself was associated strongly with trust in the lexicon skewed the results and were not representative of the level of overall trust in the novel. Therefore we opted to remove the term from the lexicon.

On the other hand, FEIL contains mostly contemporary words and their contemporary emotion associations. It is reasonable to assume that these words and their associations would have been subject to semantic shift. Hence we needed to ensure that first and foremost the most common words in our texts that in our subjective opinion have an emotion association are indeed in the lexicon, and secondly that the most common words that match words in the emotion lexicon are labeled correctly for emotions at reasonable intensities. These two steps are iterative and continuous in that they should be repeated whenever the lexicon or lemmatization is altered.

Removing words that carry little to no emotion association is fairly unproblematic, however, altering emotion labels or intensity scores or adding new words to the lexicon should be avoided. If necessary, such additive alterations require the use of multiple annotators who are not the authors and cross-checking the results using inter-annotator agreement scores [START_REF] Wouter Van Atteveldt | The validity of sentiment analysis: Comparing manual annotation, crowdcoding, dictionary approaches, and machine learning algorithms[END_REF].

For this reason, we did not want to introduce new biases into the lexicon based our own interpretations of emotion intensities. Thus we developed an alternative method that would allow us to easily and objectively add words to the lexicon. To enable this we created word embeddings of our texts and used them to look up words in the lexicon with high cosine similarity to the words we wanted to introduce to the lexicon (as per e.g. [START_REF] Maas | Learning word vectors for sentiment analysis[END_REF][START_REF] Yu | Refining word embeddings using intensity scores for sentiment analysis[END_REF][START_REF] Ye | Encoding sentiment information into word vectors for sentiment analysis[END_REF]. This lead to the association for e.g. the words kirkas, valkoinen, and valkea (clear, white, white/light/bright often referring to fire or morning light) to be identical.

Translation

The provost sits down in his rocking chair, stands his pipe on the floor against the table leg, and starts drinking his coffee Original Rovasti istuutuu keinutuoliinsa, panee piippunsa lattialle pöydän jalkaa vasten pystyyn ja rupeaa juomaan kahvians Murre (hist) (öljy)movasti istua keinutuoli panna pippu latija pöytä jalka vaste pystyä ja ruveta juoma kahvis spaCy (news_lg)

Rovasti istuutua keinutuoliinsa panee piippu lattia pöytä jalka vasten pystyyn ja rupeata juoda kahvians spaCy (exp. /w voikko) rovasti istuutua keinutuoli panna piippu lattia pöytä jalka vasten pystyyn ja ruveta juoda kahvians UralicNLP Rovasti|rovasti istuutua panna piippu lattia pöytä jalka vasten pystyyn|pysty ja ruveta juoma|juoda Turku Neural Parser rovasti istuutua keinu#tuoli panna piippu lattia pöytä jalka vasten pystyyn ja ruveta juoda kahvi Ideal lemmmatization rovasti istuutua keinutuoli panna piippu lattia pöytä jalka vasten pystyyn ja ruveta juoda kahvi Table 1: Example of lemmatization using different lemmatizers for Finnish.

The words that needed to be added were relatively few so we were able to manually check that their emotion associations and intensities made sense.

For future projects, we intend to employ human annotators in conjunction with word embeddings. Nonetheless, this approach alone showed much promise and was very accurate within the small sample size in both recognizing semantically similar words and in mitigating issues with semantic shift.

Ultimately we ended up removing 128 entries from the lexicon and adding 203 tokens including rakastaa, to love. As the FEIL lexicon was based on an English lexicon, this exlusion of such a central emotional term demonstrates the issue with noun and verb distinctions in Finnish compared to English. The noun and verb forms are often the same in English unlike in Finnish where the forms are distinct (cf. to love/a love, to run/a run vs. rakastaa/rakkaus, juosta/juoksu). Many of such instances were addressed in the creation of FEIL with the addition of verb forms copying the intensity scores and emotion associations of the English words, yet many verb forms are still missing from the lexicon.

We used this domain-and period-specific version of FEIL to tabulate normalized (per token count for inter-text comparability), intensity scores for each target text. Other future projects should include checking that both noun and verb forms are found in the lexicon.

The co-occurence matrix shows that emotion associations are not linear. A word associated with anger is quite likely (0.5) to also be associated with fear, but a word associated with fear is slightly less likely to be associated with anger (0.42). Words associated with sadness are highly likely to also be associated with fear, however, due to the very low number of sadness-associated words in the lexicon, fear-associated words are much less likely to simultaneously also evoke sadness (0.09). Joy is also the only purely positive emotion in the lexicon, which means it is more likely to be associated with many positive emotions beyond joy itself due to annotation process conducted with best-worst scaling [START_REF] Kiritchenko | Bestworst scaling more reliable than rating scales: A case study on sentiment intensity annotation[END_REF] (ranking words associated with a specific emotion in terms of least to most associated).

As mentioned earlier, tone and mood can be difficult to distinguish from each other and can even be intertwined to different degrees, especially if we focus on words alone. However, we argue that the tone of a literary text tends to shift much more within and between chapters, and therefore by focusing on the first paragraphs of each chapter, or even the opening paragraphs of the first chapter only, we can get a fairly accurate idea of the mood of the text due to its more stable nature, with a smaller risk of it being confused with tone.

It is well-established that first impressions matter in literature and beginnings tend to shape the experience of reading and set the mood for the whole text. Tone might vary within one text depending on changing narrative viewpoints or even narrators, or switching from descriptive language ot dialogue. Theories of perception (e.g. [START_REF] Perry | Literary dynamics: how the order of a text creates its meanings [with an analysis of faulkner's" a rose for emily[END_REF]) argue that the openings play a crucial role in creating a text's overall emotional disposition. The affective language and emotional effects created at the beginning of a text modify and adjust the reader's general emotional orientation by shaping up modes of perception and organization of information. For instance, the melancholic mood created in the beginning of Aho's Rautatie (Railroad), or the strong effects of disgust in the beginning of Sillanpää's Hurskas kurjuus (Meek Heritage), are likely to influence the reader experiences later reactions and feelings triggered by narrative events.

The Mood in Selected Texts

As the results mostly consist of a dataframe with emotion intensity scores for each text, the results do not easily lend themselves to visual representations. Therefore, we are focusing the presentation of our results on a small subset of data. We chose four texts based mostly on the second author's area of expertise and previous intimate analyses of the affective landscapes of these texts. The scores for the chosen texts' first three paragraphs are presented in table form in table 2 and f0or both approaches comparatively in figures 2 and 3.

An overview of the selected texts

The first one is Juhani Aho's breakthrough novel Rautatie (tr. as The Railroad, 1884). In this text, from the perspective of the implied reader, the novel evokes emotional effects of melancholia and nostalgia, which are characteristic of Aho's work.

The second one is Minna Canth's Kauppa-Lopo (no translation, the title refers to the protagonist's nickname, 1889), a tragic story of poverty and illness. The beginning of the novella, set in prison, underlines the anti-hero's ugly appearance, but the narrative contrasts the physical ugliness with an inner goodness: she is described as good-hearted and compassionate towards other people. The story was met with anger in contemporary audience, and the critics did not value her social criticism. Canth's naturalism was considered "poor art" by her contemporaries and she was accused of being an admirer of disgust, "destroying the laws of beauty, unfolding ugliness in every sense" (Rossi, 2007, 52).

The third one is Frans Emil Sillanpää's Hurskas kurjuus (tr. as Meek Heritage, literally "Sacred Misery", 1919), which begins with a shocking prologue which anticipates the death of the protagonist: it describes the execution of a poor tenant farmer who had ended up as a Red Guard soldier in the Finnish Civil War (1918). Despite the negative emotions and the tragic events the narrator also expresses trust and comfort in the future of the Finnish nation. When Sillanpää's novel appeared it was met with confusion.

The fourth and last one is Putkinotko (no translation, 1919-20) by Joel Lehtonen. Like Sillanpää's Sacred Misery, this novel tracks the tensions that escalated in the Finnish Civil War in 1918. The novel's protagonist, a good-hearted yet selfwilled tenant farmer resigns to obey the landlord and instead resorts to illegal distillery to support the family. The novel is emotionally ambivalent: the idyllic descriptions of Finnish summer nature and the comic elements are likely to arouse positive emotions, while the unembellished description of poverty intends to evoke moral anger and sadness over social inequality.

Results

The results for the texts are presented in figures 2 and 3.

In figure 2 we can see some patterns emerge. In particular, the laconism of Rautatie is evident when compared to the other authors and the strong early emotional impact of Hurskas Kurjuus becomes very apparent, with fear and anger, but also sadness being particularly notable. Fear and to some extent anger are also highly present in Kauppalopo, likely due to the descriptions of the prison environment and the appearance of the protago- When comparing the two different segmentations, first paragraph-only vs. opening paragraphs of each chapter, the latter shows a stronger prevalence of positive emotions. We take this to indicate that the intended opening mood for these novels is constructed on negative emotions intended to evoke strong feelings in the reader. In the former segmentation, the emotion distribution is more varied and seemingly converging on the distribution of emotion words in the lexicon.

Discussion

Our computationally derived results correspond highly with qualitative evaluations of the same target texts in terms of established interpretations of mood specifically when compared to the emotion word distribution of the first three paragraphs of a literary text. The valency and intensity of emotions in the opening paragraphs of the book and the opening paragraphs of all chapters the emotions approach the distribution of emotions in the lexicon in the former segmentation. That is, they become muddled because they are not focused enough. Only minor effects of the authors' style can be discerned when applying this method across all chapters. Not only are the differences between chapters reduced with the former, all-chapters, approach, but the differences between the texts also become less clear. This could also be in part because the focus and narrative choices become more varied and therefore the results average out and start to converge on the distribution of emotions in the lexicon. We recommend that the quest for mood should begin with the opening paragraphs of a text.

The qualitative analysis of the selected works, summarized above, has paid attention to various aspects of depicting and triggering emotions in a literary texts:

1. the characters' and the narrators' emotions 2. the emotional effects targeted at the implied reader 3. the empirical readers' reactions in contemporary reception 4. the texts' tone, the organizing feeling of a literary work, which is never reducible to a reader's emotional response to a text, nor to a text's internal representations of feeling (on the concept of the emotional effect, see [START_REF] Lyytikäinen | How to Study Emotion Effects in Literature: Written Emotions in Edgar Allan Poe's "The Fall of the House of Usher[END_REF]; on the notion of tone, see Ngai (2005, 28).

It should be noted that evoking emotional effects in literature is not restricted to emotion-associated words or to direct descriptions of the character's emotions. All facets of the narrative, from the description of objects to the narrative point of view and style, including tropes and even the rhythm of the text are important aspects in triggering emotional effects in the reader. As an example, the melancholic tone of Juhani Aho's text is not generated by themes of separation and loss alone but also by Aho's style, which favors fragmentation and loosening of syntax, with a recurring mannerism of three points "...", as a sign of hesitation and withdrawal, even evoking a depressive loss of contact.

The qualitative analysis demonstrates that the selected texts depict and trigger negative emotions in particular: feelings of deception, fear, anxiety, disgust and hatred, anger, moral indignation and melancholia. This can be partly explained by genrespecific emotional effects: a critical naturalist novel tends to shock and challenge its reader by representing and inciting strong negative emotions, which confirm the effect of the reality of a text and direct the reader's attention to the social defects described. For instance, the emotion of disgust, a genre-specific emotion of the naturalist novel, is a named emotion and salient in Sillanpää's and Canth's novels in particular [START_REF] Rossi | Le naturalisme finlandais. Une conception entropique du quotidien[END_REF][START_REF] Rossi | Writing disgust, writing realities[END_REF][START_REF] Rossi | Alkukantaisuus ja tunteet -Primitivismi 1900-luvun alun suomalaisessa kirjallisuudessa[END_REF].

The salience of negative emotions can be explained by the importance of negative emotions in literature and art in general. As discussed by [START_REF] Menninghaus | The distancing-embracing model of the enjoyment of negative emotions in art reception[END_REF] negative emotions are an important resource for the arts, since negative emotions have been shown to be particularly powerful in securing attention, intense emotional involvement, and high memorability, and hence is precisely what artworks strive for. Narrative plots routinely involve social conflicts and both represent and elicit negative emotions in response to such conflicts: failing marriages, unhappy love, long separations, adultery, betrayed friendship, and the like. In narratives, happiness is generally not described in great detail but rather evoked as a peak moment to be challenged, or as a goal to strive for: Canth and Jotuni depict the characters' desire for happiness and love, which is not possible in today's society; Sillanpää's narrator expresses trust in and hope for the future of Finland, and Aho concludes The Railroad with the normative happy ending of a fairy tale -yet this happiness is only evoked, but not described in detail.

Future Work

This dataset will be used for more robust detection of tone and mood in Finnish literature using many novel approaches. Our preliminary studies show that the "big data" results support qualitative analyses and further justify the use of purely lexicon-based methods and affect as a proxy for mood when dealing with larger collections of text where word choice is an important factor in evoking affective states in the reader. Explicitly, we can see that the choice of emotion-associated words in the first three paragraphs correlates highly with established analyses of mood in the selected texts. We hope to add established emotion categories from literary affect studies (see e.g. Hogan 2011) to the lexicon as a measure to further improve the usability of the FEIL lexicon for the literary domain (Öhman, 2020). Additionally, we would like to expand on the methodologies used in this exploratory study and hopefully create more and more robust approaches to tone and mood detection in literature and perhaps also incorporate intentionality detection [START_REF] Guo | An algorithm for detection of cognitive intentionality in text analysis[END_REF] to further separate tone from mood.

Figure 1 :

 1 Figure 1: Co-occurence of emotions in FEIL.

Figure 2 :

 2 Figure 2: Emotion word distribution in first three paragraphs per 1000 words

Table 2 :

 2 Normalized emotion scores for each novel's first three paragraphs.

	title	anger anticipation disgust fear	joy	sadness trust
	Putkinotko	4.22	8.67	5.42	11.75 15.69 1.47	22.07
	Kauppa-Lopo	12.45 5.71	7.40	19.11 7.66	0	0
	Rautatie	8.56	21.15	0	10.50 13.81 5.52	16.74
	Hurskas kurjuus 20.33 9.90	11.25	27.73 9.07	7.29	15.05

On the concepts of tone and mood in literary studies, see[START_REF] Richards | Practical Criticism[END_REF];[START_REF] Ngai | Ugly feelings[END_REF];[START_REF] Flatley | Affective mapping: melancholia and the politics of modernism[END_REF].

Presumably in order of entry to the database.

https://www.gutenberg.org/

https://libraries.io/pypi/ gutenberg-cleaner

All the terms roughly translate to "translator" or "translated".

The original: https://pypi.org/project/ chapterize/ and the Finnish version: https: //github.com/esohman/chapterize-fi

http://turkunlp.org/ Turku-neural-parser-pipeline/

Acknowledgements

This work was supported by JSPS KAKENHI Grant Number 22K18154.