This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing translation of (...) the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above. (shrink)

We define a multi-modal version of Computation Tree Logic ( ctl ) by extending the language with path quantifiers E δ and A δ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a ctl axiomatisation for each dimension. Completeness is proved by employing the completeness result for ctl to obtain a model along each dimension in turn. We also (...) show that the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for ctl. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional ctl logic. (shrink)

We define a multi-modal version of Computation Tree Logic (CTL) by extending the language with path quantifiers $E^\delta $ and $E^\delta $ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a CTL axiomatisation for each dimension. Completeness is proved by employing the completeness result for CTL to obtain a model along each dimension in turn. We also show that (...) the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for CTL. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional CTL logic. (shrink)

We define a multi-modal version of Computation Tree Logic (ctl) by extending the language with path quantifiers E δ and A δ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a ctl axiomatisation for each dimension. Completeness is proved by employing the completeness result for ctl to obtain a model along each dimension in turn. We also show that (...) the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for ctl. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional ctl logic. (shrink)

We define a multi-modal version of Computation Tree Logic (ctl) by extending the language with path quantifiers E δ and A δ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a ctl axiomatisation for each dimension. Completeness is proved by employing the completeness result for ctl to obtain a model along each dimension in turn. We also show that (...) the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for ctl. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional ctl logic. (shrink)

The paper presents a compositional approach to the verification of CTL* properties over reactive systems. Both symbolic model-checking and deductive verification are considered. Both methods are based on two decomposition principles. A general state formula is decomposed into basic state formulas which are CTL* formulas with no embedded path quantifiers. To deal with arbitrary basic state formulas, we introduce another reduction principle which replaces each basic path formula, i.e., path formulas whose principal operator is temporal and which contain no embedded (...) temporal operators or path quantifiers, by a newly introduced boolean variable which is added to the system. Thus, both the algorithmic and the deductive methods are based on two statification transformations which successively replace temporal formulas by assertions which contain no path quantifiers or temporal operators. Performing these decompositions repeatedly, we remain with basic assertional formulas, i.e., formulas of the form Efp and Afp for some assertion p. In the model-checking method we present a single symbolic algorithm to verify both universal and existential basic assertional properties. In the deductive method we present a small set of proof rules and show that this set is sound and relatively complete for verifying universal and existential basic assertional properties over reactive systems. Together with two proof rules for the decompositions, we obtain a sound and relatively complete proof system for arbitrary CTL* properties. Interestingly, the deductive approach for CTL* presented here, offers a viable new approach to the deductive verification of arbitrary LTL formulas. The paper corrects a previous preliminary version of a deductive system for CTL*, in which some of the rules were unsound. The correction is based on the introduction of a new type of temporal testers which are guaranteed to be non blocking. That is, when composed with a deadlock-free system, which is a key operation in the verification process, the resulting composed system is guaranteed to remain deadlock free. (shrink)

The aim of this paper is to present the activities and research methodologies of CTL, a laboratory of the Scuola Normale Superiore of Pisa, founded and directed by Lina Bolzoni. CTL’s objective is to investigate the complex structure of relationships between the linguistic and the figurative code in literary tradition, paying particular attention to the XVth, XVIth and XVIIth centuries and using information technologies both as an auxiliary research tool and as a medium for scientific dissemination. Here I shall be (...) discussing the Centre’s digitalization projects, and in particular the project concerned with the Orlando Furioso and its remediation into images. This project, active since 2007, is, I believe, particularly representative of the progressive implementation within CTL of both traditional and computer-related methodologies in the planning of digital collections dedicated to words and images. (shrink)

A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$-trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL$^{*}$ into CTL$_{rp}$. In particular, that yields a complete axiomatization for the translations of all valid CTL$^{*}$-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium for reasoning (...) about branching time. (shrink)

Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as "Alternating-time Temporal Logic". The key insight in (...) ATL is that the path quantifiers of CTL could be replaced by "cooperation modalities", of the form $\langle \langle \Gamma \rangle \rangle $, where Γ is a set of agents. The intended interpretation of an ATL formula $\langle \langle \Gamma \rangle \rangle \varphi $ is that the agents Γ can cooperate to ensure that φ holds. In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as "group Γ can cooperate to bring about φ iff it is common knowledge in Γ that ψ". The resulting logic -- Alternating-time Temporal Epistemic Logic -- shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems. (shrink)

In this paper we present BTC, which is a complete logic for branchingtime whose modal operator quantifies over histories and whose temporal operators involve a restricted quantification over histories in a given possible choice. This is a technical novelty, since the operators of the usual logics for branching-time such as CTL express an unrestricted quantification over histories and moments. The value of the apparatus we introduce is connected to those logics of agency that are interpreted on branching-time, as for instance (...) Stit Logics. (shrink)

The Communicational Theory of Law (CTL) usually differentiates between Legal Sociology and Legal Theory, in the sense that Legal Sociology is concerned with the social validity of the rules and Legal Theory with the formal or legal validity of the rules. It can be argued that both disciplines are two different perspectives of the same empirical reality (legal rules). Also, legal System and social milieu are two closely linked realities; they cannot be separated because they need each other. The Law (...) is the form or order that the social milieu takes, and, at the same time, the social environment provides the ideas, collective representations and other matters that need a legal regulation. For this reason, the epistemological separation between Sociology and Legal Theory must be overcome when the theoretical perspective comes to legal decisions. Thus, the decisional moment becomes the meeting point between the legal System and the social milieu. This is where the concept of the legal System fulfils its main function, as it allows for the dynamism and adaptability of the legal order. The hermeneutic re-elaboration of the normative texts will be the channel through which the social facts and other material elements can inform the meaning or possible interpretations of the rules and institutions of the legal order. This happens primarily by influencing theoretical and doctrinal works of an expository and didactic nature; and secondarily by influencing the decisions of legal operators and courts. This study seeks to explain how the social context influences legal decisions and the formation of the legal System, from a communicational perspective of Law. In order to do so, it will be necessary to set out two epistemological premises of CTL: the semiotic tripartition of the Theory of Law and the legal Order-legal System distinction. (shrink)

We give a sound and complete axiomatization for the full computation tree logic, CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.

We present a temporal logic of branching time with four primitive operators: |$\exists {\mathcal {C}}$| – it may change whether; |$\forall {\mathcal {C}} $| – it must change whether; |$\exists \Box $| – it may be endlessly unchangeable that; and |$\forall \Box $| – it must be endlessly unchangeable that. Semantically, operator |$\forall {\mathcal {C}}$| expresses a change in the logical value of the given formula in every state that may be an immediate successor of the one considered, while |$\exists (...) {\mathcal {C}}$| expresses a change in the logical value of the given formula in some state that is a possible immediate successor. |$\forall {\mathcal {C}} $| and |$\exists {\mathcal {C}}$| are not normal operators, they are not mutually definable and have unusual properties: |$\forall {\mathcal {C}} A\leftrightarrow \forall {\mathcal {C}} \neg A$| and |$\exists {\mathcal {C}} A \leftrightarrow \exists {\mathcal {C}} \neg A$| are axioms. Operators |$\exists \Box $| and |$\forall \Box $| express endless unchangeability in some and all paths, respectively. Our axiomatization contains two infinitary rules that allow one to obtain |$\exists \Box A$| from infinitely many combinations of formulas with |$A, \neg, \forall {\mathcal {C}}, \land $|⁠, and to get |$\forall \Box A$| from infinitely many combinations of formulas with |$A, \neg, \exists {\mathcal {C}}, \land $|⁠. We show that our formalism is complete by presenting a bridge between our logic and logic |$\textsf {UB}$|⁠, which is a fragment of |$\textsf {CTL}$| in which until operators does not occur. (shrink)

Graphs are among the most frequently used structures in Computer Science. Some of the properties that must be checked in many applications are connectivity, acyclicity and the Eulerian and Hamiltonian properties. In this work, we analyze how we can express these four properties with modal logics. This involves two issues: whether each of the modal languages under consideration has enough expressive power to describe these properties and how complex it is to use these logics to actually test whether a given (...) graph has some desired property. First, we show that these properties are not definable in a basic modal logic or in any bisimulation-invariant extension of it, like the modal μ-calculus. We then show that it is possible to express some of the above properties in a basic hybrid logic. Unfortunately, the Hamiltonian and Eulerian properties still cannot be efficiently checked. In a second attempt, we propose an extension of CTL* with nominals and show that the Hamiltonian property can be more efficiently checked in this logic than in the previous one. In a third attempt, we extend the basic hybrid logic with the ↓ operator and show that we can check the Hamiltonian property with optimal complexity in this logic. Finally, we tackle the Eulerian property in two different ways. First, we develop a generic method to express edge-related properties in hybrid logics and use it to express the Eulerian property. Second, we express a necessary and sufficient condition for the Eulerian property to hold using a graded modal logic. (shrink)

ABSTRACTIndividual differences in the habitual use of emotion regulation strategies may play a critical role in understanding psychological and biological stress reactivity and recovery in depression and anxiety. This study investigated the relation between the habitual use of different emotion regulation strategies and cortisol reactivity and recovery in healthy control individuals and in individuals diagnosed with social anxiety disorder. The tendency to worry was associated with increased cortisol reactivity to a stressor across the full sample. Rumination was not associated with (...) cortisol reactivity, despite its oft-reported similarities to worry. Worry and rumination, however, were associated with increased cortisol during recovery from the stressor. The only difference between CTL and SAD participants was observed for reappraisal. In the CTL but not in the SAD group, reappraisal predicted recovery, such that an increased tendency to reappraise was associated with greater c... (shrink)

Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as Alternating-time Temporal Logic (ATL). The key insight (...) in ATL is that the path quantifiers of CTL could be replaced by cooperation modalities, of the form , where is a set of agents. The intended interpretation of an ATL formula is that the agents can cooperate to ensure that holds (equivalently, that have a winning strategy for ). In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as group can cooperate to bring about iff it is common knowledge in that . The resulting logic — Alternating-time Temporal Epistemic Logic (ATEL) — shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems. (shrink)

In program synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. When the system is open, then at each moment it reads input signals and writes output signals, which depend on the input signals and the history of the computation so far. The specification considers all possible input sequences. Thus, if the specification is linear, it should hold in every computation generated by the interaction, and if the specification is branching, it should hold in (...) the tree that embodies all possible input sequences. Often, the system cannot read all the input signals generated by its environment. For example, in a distributed setting, it might be that each process can read input signals of only part of the underlying processes. Then, we should transform a specification into a system whose output depends only on the readable parts of the input signals and the history of the computation. This is called synthesis with incomplete information. In this work we solve the problem of synthesis with incomplete information in its full generality. We consider linear and branching settings with complete and incomplete information. We claim that alternation is a suitable and helpful mechanism for coping with incomplete information. Using alternating tree automata, we show that incomplete information does not make the synthesis problem more complex, in both the linear and the branching paradigm. In particular, we prove that independently of the presence of incomplete information, the synthesis problems for CTL and CTL * are complete for EXPTIME and 2EXPTIME, respectively. (shrink)

DEBATE MULTICULTURAL - etnia, clase y nación.h2 { margin-right: 0.11cm; margin-top: 0.07cm; margin-bottom: 0cm; color: rgb(74, 106, 166); page-break-after: auto; }h2.western { font-family: "Arial",sans-serif; font-size: 10pt; }h2.cjk { font-family: "DejaVu Sans"; font-size: 10pt; }h2.ctl { font-family: "Arial",sans-serif; font-size: 10pt; }p { margin-bottom: 0.21cm; }.

The main result of the present paper is that the variable-free fragment of logic K*, the logic with a single K-style modality and its “reflexive and transitive closure,” is EXPTIMEcomplete. It is then shown that this immediately gives EXPTIME-completeness of variable-free fragments of a number of known EXPTIME-complete logics. Our proof contains a general idea of how to construct a polynomial-time reduction of a propositional logic to its n-variable—and even, in the cases of K*, PDL, CTL, ATL, and some others, (...) variable-free—fragments. Complexity of countermodels for such fragments is considered. (shrink)

We present a framework for verifying systems composed of heterogeneous reasoning agents, in which each agent may have differing knowledge and inferential capabilities, and where the resources each agent is prepared to commit to a goal (time, memory and communication bandwidth) are bounded. The framework allows us to investigate, for example, whether a goal can be achieved if a particular agent, perhaps possessing key information or inferential capabilities, is unable (or unwilling) to contribute more than a given portion of its (...) available computational resources or bandwidth to the problem. We present a novel temporal epistemic logic, BMCL-CTL , which allows us to describe a set of reasoning agents with bounds on time, memory and the number of messages they can exchange. The bounds on memory and communication are expressed as axioms in the logic. As an example, we show how to axiomatise a system of agents which reason using resolution and prove that the resulting logic is sound and complete. We then show how to encode a simple system of reasoning agents specified in BMCL-CTL in the description language of the Mocha model checker (Alur et al., Proceedings of the tenth international conference on computer-aided verification (CAV) , 1998), and verify that the agents can achieve a goal only if they are prepared to commit certain time, memory and communication resources. (shrink)

The satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations. It is shown that FO 2 over ordered, respectively wellordered, domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially (...) the same as for plain unconstrained FO 2 , namely non-deterministic exponential time. In contrast FO 2 becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as orderings, wellorderings, or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO 2 and computation tree logic CTL. (shrink)

Researchers have postulated that deficits in cognitive control are associated with, and thus may underlie, the perseverative thinking that characterises generalised anxiety disorder. We examined associations between cognitive control and levels of spontaneous state rumination following a stressor in a sample of healthy control participants and participants with GAD. We assessed cognitive control by measuring working memory capacity, defined as the ability to maintain task-relevant information by ignoring task-irrelevant information. To this end, we used an affective version of the reading (...) span task with valenced distractors. Lower WMC in the presence of negative distractors was associated with greater state rumination in the GAD group, but not in the CTL group. These findings suggest that difficulty maintaining task-relevant information due to interference from negative distractors contributes to perseverative thinking in GAD. (shrink)

Sound and complete axiomatizations are provided for a number of different logics involving modalities for the knowledge of multiple agents and operators for branching time, extending previous work of Halpern, van der Meyden and Vardi [to appear, SIAM Journal on Computing] for logics of knowledge and linear time. The paper considers the system constraints of synchrony, perfect recall and unique initial states, which give rise to interaction axioms. The language is based on the temporal logic CTL*, interpreted with respect to (...) a version of the bundle semantics. (shrink)

Sound and complete axiomatizations are provided for a number of different logics involving modalities for the knowledge of multiple agents and operators for branching time, extending previous work of Halpern, van der Meyden and Vardi [to appear, SIAM Journal on Computing] for logics of knowledge and linear time. The paper considers the system constraints of synchrony, perfect recall and unique initial states, which give rise to interaction axioms. The language is based on the temporal logic CTL*, interpreted with respect to (...) a version of the bundle semantics. (shrink)

Although formal system verification has been around for many years, little attention was given to the case where the specification of the system has to be changed. This may occur due to a failure in capturing the clients’ requirements or due to some change in the domain (think for example of banking systems that have to adapt to different taxes being imposed). We are interested in having methods not only to verify properties, but also to suggest how the system model (...) should be changed so that a property would be satisfied. For this purpose, we will use techniques from the area of Belief Revision, that deals with the problem of changing a knowledge base in view of new information. In the last thirty years, several authors have contributed with change operations and ways of characterizing them. However, most of the work concentrates on knowledge bases represented using classical propositional logic. In the last decade, there have been efforts to apply belief revision theory to description and modal logics. In this work, we analyze what is needed for a theory of belief revision which can be applied to the temporal logic, such as the Computation Tree Logic (CTL). In particular, we illustrate different alternatives for formalizing the concept of revision of CTL. Our interest in this particular logic comes both from practical issues, since it is used for software specification, as from theoretical issues, as it is a non-compact logic and most existing results rely on compactness. We focus here on the revision of CTL models and present a characterization result for the revision of partial models. (shrink)

We consider weighted o-minimal hybrid systems, which extend classical o-minimal hybrid systems with cost functions. These cost functions are “observer variables” which increase while the system evolves but do not constrain the behaviour of the system. In this paper, we prove two main results: optimal o-minimal hybrid games are decidable; the model-checking of WCTL, an extension of CTL which can constrain the cost variables, is decidable over that model. This has to be compared with the same problems in the framework (...) of timed automata where both problems are undecidable in general, while they are decidable for the restricted class of one-clock timed automata. (shrink)

Theiler's virus is a picornavirus of mouse which causes an acute encephalomyelitis followed by a persistent infection of the white matter resulting in chronic inflammation and demyelination. This disease has been studied as a model for multiple sclerosis. Inbred strains of mice are either resistant--they clear the infection after the acute encephalomyelitis--or susceptible to persistent infection and demyelination. Susceptibility is a polygenic trait which has been analyzed using methods of association with “candidate” genes, and linkage analysis after a complete genome (...) scan. The H-2Db gene is responsible for an efficient CTL response which makes some strains resistant. Non H-2 genes responsible for the susceptibility of other strains have been mapped by linkage analysis to the Ifng and, possibly, the Mbp loci. The analysis of a set of congenic mice ruled out the possiblity that the relevant gene codes for interferon gamma, and showed that the region around Ifngprobably contains two susceptibility genes. The analysis of mutant mice showed further that the Mbp gene, which codes for the myelin basic protein, has a major effect on viral persistence. BioEssays 20:627–633, 1998. © 1998 John Wiley & Sons Inc. (shrink)

P { margin-bottom: 0.21cm; direction: ltr; color: rgb; widows: 2; orphans: 2; }P.western { font-family: "Times New Roman",serif; font-size: 12pt; }P.cjk { font-family: "Times New Roman",serif; font-size: 12pt; }P.ctl { font-family: "Times New Roman",serif; font-size: 12pt; } Hegel's transient notion of "Aether", developed and finally abandoned again during his short period of time at the University of Jena in the early years of the 19th century, has received comparatively little attention so far – much less than, for example, his Phenomenology (...) of Spirit, or his later systematic works which he published after his departure from Jena. In modern and contemporary physics, on the other hand, novel notions comparable to Hegel's "aether" have become interesting again with the rise of quantum physics. In this essay we recapitulate and explain the notion of "Aether" in Hegel's works and compare it to novel aether concepts which might be appropriate in the context of contemporary quantum physics. Such a juxtaposition would well have matched Hegel's own intentions, since he had always been a keen observer of the latest developments in the natural sciences during his own lifetime. In conclusion we can say that, in spite of a number of differences, both notions of aether can be speculatively characterised by the paradoxical term "reality of possibility". (shrink)

This paper compares the recently proposed Robust Full Computational Tree Logic to model robustness in concurrent systems with other computational tree logic -based logics. RoCTL* extends CTL* with the addition of the operators Obligatory and Robustly, which quantify over failure-free paths and paths with one more failure respectively. This paper focuses on examining the succinctness and expressiveness of RoCTL* by presenting translations to and from RoCTL*. The core result of this paper is to show that RoCTL* is expressively equivalent to (...) CTL* but is non-elementarily more succinct. That is, RoCTL* does not add any expressive power over CTL*, but can represent some properties using vastly reduced formulae. We present a translation from RoCTL* into CTL* that preserves truth but may result in non-elementary growth in the length of the translated formula, as each nested Robustly operator may result in an extra exponential blowup. However, we show that this translation is optimal in the sense th.. (shrink)

$LTL is a version of linear temporal logic in which eventualities are not expressible, but in which there is a sentential constant $ intended to be true just at the end of some behaviour of interest—that is, to mark the end of the accepted words of some language. There is an effectively recognisable class of $LTL formulae which express behaviours, but in a sense different from the standard one of temporal logics like LTL or CTL. This representation is useful for (...) solving a class of decision processes with temporally extended goals, which in turn are useful for representing an important class of AI planning problems. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Photo-credit to Chicago Sun-Times and James Mescall. 4 "The town is beastly and the weather was vile": Bertrand Russell in Chicago, 1938-1939 Visiting Chicago in 1867, Lord Amberley offered his wife an appreciation of the city: "The country around Chicago is flat and ugly; the town itself has good buildings but has a rough unfinished appearance which does not contribute to its attractions."l While Bertrand Russell is known to (...) have accepted and developed particular aspects of his father's thought, it is more likely that his own visits to Chicago, rather than this nineteenth -century appraisal, brought him to the opinion that "the town is beastly and the weather was vile."z One might suppose Russell's longest stay reaffirmed his image of the city suggested in a 1922 article expressing fear of "a slow destruction of the civilization of China" through which "the big towns will become like Chicago."3 Here, Russell appears to have envisioned this city as an amorphous collection of streets and structures manifesting the least desirable values of American capitalism. In his Autobiography a single paragraph is devoted to his 1938-1939 experience of "the bleak hideousness of Chicago" (II, p. 332). Yet there was far more to Russell's six-month sojourn than the little he chose to recall in print. One-half year is a significant period in anyone's life, even for a man who lived ninety-seven (and a half) years. This article, then, presents an account of Russell's coming to and departure from Chicago and his diverse activities while a professor at the University of Chicago. The need to secure some permanent academic position was strongly felt by Russell in the mid-1930s. His ~aertrand and Patricia Russell, The Amberley Papers (London: Allen and Unwin, 1966), p. 57. zThe Autobiography of Bertrand Russell (Boston: Atlantic-Little, Brown, 1968), II, p. 332. 3"How Washington Can Help China", New Republic, 4 Jan. 1922, p. 154. / 5 second marriage had ended and a third was beginn~ng; ~ar­ ticipation in the Beacon Hill experimen~ w~s behlnd hlmj and journalistic writing, though ~ contlnulng so~rce of income, was ceasing to be attractlve: No~ a d~slre to return to philosophical work, recurrlng fl~anclal troubles, and the fear of another, far m~r~ destr~ctlve.European~ar all contributed toward his declslon to lnvestlgate Amerlcan possibilities. My feelings are threefold: (a) I' have a lot of ideas in,my head that I long to work at and believe important (b) I am faced with such poverty that I may be unable to give a proper education to the child that is coming (c) That Europe is no place for children with the imminent risk of war--particularly England, which is ' 4 likely to suffer most in the next war. At first, with the help of his American publisher, Warder Norton, Russell approached Princeton University hoping for a research post "on the foundations of mathematics and philosophy" (letter to Norton, 13 Jan. 1937). But no prospect materialized, and he requested Norton to inquire at universities such as Columbia and Harvard. Finally in the spring of 1937 Russell received a letter from Professor Scott Buchanan who then represented the University of Chicago's Committee on the Liberal Arts (COTLA). Buchanan offered a place on COTLA with only minor teaching duties. Writing to Norton that this "seems a very agreeable job", Russell nevertheless suggested the post "may be reactionary and the sort of thing my radical friends would think I ought not to be connected with. '" it is a committee concerned with a conservative reform of education." But the invitation promised adequate time for independent research, and Russell, quite characteristically, concluded "my wish is to accept, but not if doing so would be wicked" (letter of 30 Apr. 1937). However, Buchanan, having soon thereafter left the University of Chicago for a Maryland college, corresponded no further with Russell. The COTLA job offer was officially withdrawn. Only in January 1938 did Russell again hear from a University of Chicago spokesman. Aware that Russell had been somewhat brusquely treated, Professor Richard P. McKeon of the Department of Philosophy now wrote "in the... (shrink)

ABSTRACT A complete axiomatic system CTLrp is introduced for a temporal logic for finitely branching ω+ -trees in a language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL* into CTLrp. In particular, that yields a complete axiomatization for the translations of all valid CTL*-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium for (...) reasoning about branching time. (shrink)

It is known that the full computation-tree logic CTL * is an important base logic for model checking. The bisimulation theorem for CTL* is known to be useful for abstraction in model checking. In this paper, the bisimulation theorems for two paraconsistent four-valued extensions 4CTL* and 4LCTL* of CTL* are shown, and a translation from 4CTL* into CTL* is presented. By using 4CTL* and 4LCTL*, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.

It is known that the full computation-tree logic CTL∗is an important base logic for model checking. The bisimulation theorem for CTL∗is known to be useful for abstraction in model checking. In this paper, thebisimulation theorems for two paraconsistent four-valued extensions 4CTL∗and 4LCTL∗of CTL∗are shown, and a translation from 4CTL∗into CTL∗ispresented. By using 4CTL∗and 4LCTL∗, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.

Interferon (IFN) induced during a virus infection mediates antiviral effects both by direct inhibition of virus replication and by influencing the proliferation, differentiation, and chemotaxis of cyto‐toxic lymphocytes which control the infection. Cells from tissue taken from virus‐infected mice are conditioned by IFN to resist lysis by natural killer (NK) cells, while they become increasingly susceptible to lysis by cytotoxic Tlymphocytes (CTL). This is due to marked IFN‐induced biochemical changes, including an up‐regulation of major histocompatibility antigens, which are targets for (...) CTL. Cytopathic viruses, which inhibit cellular RNA and protein synthesis, render target cells refractory to IFN‐mediated protection against NK cells, thereby providing a mechanism for NK cells to mediate antiviral effect by preferentially lysing virus‐infected but not uninfected cells. (shrink)

We present the first-order logic of change, which is an extension of the propositional logic of change $\textsf {LC}\Box $ developed and axiomatized by Świętorzecka and Czermak. $\textsf {LC}\Box $ has two primitive operators: ${\mathcal {C}}$ to be read it changes whether and $\Box $ for constant unchangeability. It implements the philosophically grounded idea that with the help of the primary concept of change it is possible to define the concept of time. One of the characteristic axioms for ${\mathcal {C}}$ (...) is ${\mathcal {C}} A \to {\mathcal {C}}\neg A$ and one of the primitive rules is $\omega $-rule introducing $\Box $. It turns out that the next operator is definable in $\textsf {LC}\Box $. Logic $\textsf {LC}\Box $ with next is equivalent to certain fragment of $\textsf {LTL}$ extended by the appropriate definition of ${\mathcal {C}}$. Recently, $\textsf {LC}\Box $ has also been modified to the propositional logic of ‘branching’ changes $\textsf {BTC}$ by Łyczak and the logic of ‘parallel’ changes $\textsf {LC}\Box $ ↳ by Świętorzecka and Łyczak. Extended in an appropriate manner, $\textsf {BTC}$ is equivalent to a certain fragment of logic $\textsf {CTL}$ to which definitions of two kinds of changes have been added. Here we propose an extension of $\textsf {LC}\Box $ to first-order logic in which, again, the only primitive modal operators are ${\mathcal {C}}$ and $\Box $. We interpret our logic in the semantics of histories of changes. We give an axiomatic system $\textsf {LC}\Box Q$ for the considered logic, and we show selected theses about some relationships between ${\mathcal {C}}$, $\Box $ and $\forall $. Then we prove the completeness of $\textsf {LC}\Box Q$. Finally, we compare our logic with $\textsf {FOLT}$ and show the relation between $\textsf {LC}\Box Q$ and a certain fragment of the Kröger system $\varSigma $ to which the definition of ${\mathcal {C}}$ was added. (shrink)

We present an introductory survey of temporal and dynamic logics: logics for reasoning about how environments change over time, and how dynamic processes affect their environments.We begin by introducing the historical development of temporal and dynamic logic, starting with the seminal work of Prior. This leads to a discussion of the use of temporal and dynamic logic in computer science. We describe LTL, CTL, and PDL; three key formalisms used in computer science for reasoning about programs, and illustrate how these (...) formalisms may be used in the formal specification and verification of computer systems.We then discuss interval temporal logics.We conclude with some pointers for further reading. (shrink)

While classical temporal logics lose track of a state as soon as a temporal operator is applied, several branching-time logics able to repeatedly refer to a state have been introduced in the literature. We study such logics by introducing a new formalism, hybrid branching-time logics, subsuming the other approaches and making the ability to refer to a state more explicit by assigning a name to it. We analyze the expressive power of hybrid branching-time logics and the complexity of their satisfiability (...) problem. As main result, the satisfiability problem for the hybrid versions of several branching-time logics is proved to be 2EXPTIME -complete. To prove the upper bound, the automata-theoretic approach to branching-time logics is extended to hybrid logics. As a result of independent interest, the nonemptiness problem for alternating one-pebble Büchi tree automata is shown to be 2EXPTIME -complete. A common property of the logics studied is that they refer to only one state. This restriction is crucial: The ability to refer to more than one state causes a nonelementary blow-up in complexity. In particular, we prove that satisfiability for NCTL * has nonelementary complexity. (shrink)

Normative arrow update logic (NAUL) is a logic that combines normative temporal logic (NTL) and arrow update logic (AUL). In NAUL, norms are interpreted as arrow updates on labeled transition systems with a CTL-like logic. We show that the satisfiability problem of NAUL is decidable with a tableau method and it is in EXPSPACE.