Temporal Logics of Repeating Values

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this article, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics that suggests such a restricted use of the freeze operator. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets by proposing a symbolic representation of models. This is a quite surprising result in view of the expressive power of the logic since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier. The article also contains developments about the relationships between temporal logics with the freeze operator and counter automata as well as reductions into first-order logics over data words.

A decidable temporal logic with repeating values

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets. This is a surprising result since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier.

Counter-free input-determined timed automata

We identify a class of timed automata, which we call counter-free input-determined automata, which characterize the class of timed languages definable by several timed temporal logics in the literature, including MTL. We make use of this characterization to show that MTL+Past satisfies an “ultimate stability” property with respect to periodic sequences of timed words. Our results hold for both the pointwise and continuous semantics. Along the way we generalize the result of McNaughton-Papert to show a counter-free automata characterization of FO-definable finitely varying functions.

On continuous timed automata with input-determined guards

We consider a general class of timed automata parameterized by a set of “input-determined” operators, in a continuous time setting. We show that for any such set of operators, we have a monadic second order logic characterization of the class of timed languages accepted by the corresponding class of automata. Further, we consider natural timed temporal logics based on these operators, and show that they are expressively equivalent to the first-order fragment of the corresponding MSO logics. As a corollary of these general results we obtain an expressive completeness result for the continuous version of MTL.

Automata and logics over finitely varying functions

We extend some of the classical connections between automata and logic due to Büchi (1960) [5] and McNaughton and Papert (1971) [12] to languages of finitely varying functions or “signals”. In particular, we introduce a natural class of automata for generating finitely varying functions called View the MathML source’s, and show that it coincides in terms of language definability with a natural monadic second-order logic interpreted over finitely varying functions Rabinovich (2002) [15]. We also identify a “counter-free” subclass of View the MathML source’s which characterise the first-order definable languages of finitely varying functions. Our proofs mainly factor through the classical results for word languages. These results have applications in automata characterisations for continuously interpreted real-time logics like Metric Temporal Logic (MTL) Chevalier et al. (2006, 2007) [6] and [7].

Temporal variation of tonal spectrum of tambura

Tambura is an essential drone accompaniment used in Indian music concerts. It acts as an immediate reference of pitch for both the artists and listeners. The four strings of Tambura are tuned to the frequency ratio :1:1: . Careful listening to Tambura sound reveals that the tonal spectrum is not stationary but is time varying. The object of this study is to make a detailed spectrum analysis to find out the nature of temporal variation of the tonal spectrum of Tambura sound. Results of the analysis are correlated with perceptual evaluation conducted in a controlled acoustic environment. A significant result of this study is to demonstrate the presence of several notes which are normally not noticed even by a professional artist. The effect of bridge in Tambura in producing the so called “live tone” is explained through time and frequency parameters of Tambura sounds.

Urban Growth Analysis Using Spatial and Temporal Data

Urban growth identification, quantification, knowledge of rate and the trends of growth would help in regional planning for better infrastructure provision in environmentally sound way. This requires analysis of spatial and temporal data, which help in quantifying the trends of growth on spatial scale. Emerging technologies such as Remote Sensing, Geographic Information System (GIS) along with Global Positioning System (GPS) help in this regard. Remote sensing aids in the collection of temporal data and GIS helps in spatial analysis. This paper focuses on the analysis of urban growth pattern in the form of either radial or linear sprawl along the Bangalore - Mysore highway. Various GIS base layers such as builtup areas along the highway, road network, village boundary etc. were generated using collateral data such as the Survey of India toposheet, etc. Further, this analysis was complemented with the computation of Shannon's entropy, which helped in identifying prevalent sprawl zone, rate of growth and in delineating potential sprawl locations. The computation Shannon's entropy helped in delineating regions with dispersed and compact growth. This study reveals that the Bangalore North and South taluks contributed mainly to the sprawl with 559% increase in built-up area over a period of 28 years and high degree of dispersion. The Mysore and Srirangapatna region showed 128% change in built-up area and a high potential for sprawl with slightly high dispersion. The degree of sprawl was found to be directly proportional to the distances from the cities.

Inferring neuronal network connectivity from spike data: A temporal data mining approach

Understanding the functioning of a neural system in terms of its underlying circuitry is an important problem in neuroscience. Recent d evelopments in electrophysiology and imaging allow one to simultaneously record activities of hundreds of neurons. Inferring the underlying neuronal connectivity patterns from such multi-neuronal spike train data streams is a challenging statistical and computational problem. This task involves finding significant temporal patterns from vast amounts of symbolic time series data. In this paper we show that the frequent episode mining methods from the field of temporal data mining can be very useful in this context. In the frequent episode discovery framework, the data is viewed as a sequence of events, each of which is characterized by an event type and its time of occurrence and episodes are certain types of temporal patterns in such data. Here we show that, using the set of discovered frequent episodes from multi-neuronal data, one can infer different types of connectivity patterns in the neural system that generated it. For this purpose, we introduce the notion of mining for frequent episodes under certain temporal constraints; the structure of these temporal constraints is motivated by the application. We present algorithms for discovering serial and parallel episodes under these temporal constraints. Through extensive simulation studies we demonstrate that these methods are useful for unearthing patterns of neuronal network connectivity.

Extending temporal simulations

Direct numerical simulations (DNS) of spatially growing turbulent shear layers may be performed as temporal simulations by solving the governing equations with some additional terms while imposing streamwise periodicity. These terms are functions of the means whose spatial growth is calculated easily and accurately from statistics of the temporal DNS. Equations for such simulations are derived.

Context-dependency of a complex fruit-frugivore mutualism: temporal variation in crop size and neighborhood effects

The quantity of fruit consumed by dispersers is highly variable among individuals within plant populations. The outcome Of Such selection operated by firugivores has been examined mostly with respect to changing spatial contexts. The influence of varying temporal contexts on frugivore choice, and their possible demographic and evolutionary consequences is poorly understood. We examined if temporal variation in fruit availability across a hierarchy of nested temporal levels (interannual, intraseasonal, 120 h, 24 h) altered frugivore choice for a complex seed dispersal system in dry tropical forests of southern India. The interactions between Phyllanthus emblica and its primary disperser (ruminants) was mediated by another frugivore (a primate),which made large quantities of fruit available on the ground to ruminants. The direction and strength of crop size and neighborhood effects on this interaction varied with changing temporal contexts.Fruit availability was higher in the first of the two study years, and at the start of the season in both years. Fruit persistence on trees,determined by primate foraging, was influenced by crop size andconspecific neighborhood densities only in the high fruit availability year. Fruit removal by ruminants was influenced by crop size in both years and neighborhood densities only in the high availability year. In both years, these effects were stronger at the start of the season.Intraseasonal reduction in fruit availability diminished inequalities in fruit removal by ruminants and the influence of crop size and fruiting neighborhoods. All trees were not equally attractive to frugivores in a P. emblica population at all points of time. Temporal asymmetry in frugivore-mediated selection could reduce potential for co-evolution between firugivores and plants by diluting selective pressures. Inter-dependencies; formed between disparate animal consumers can add additional levels of complexity to plant-frugivore mutualistic networks and have potential reproductive consequences for specific individuals within populations.

A dynamical approach to the spatio-temporal features of the Portevin-Le Chatelier effect

We show that the extended Ananthakrishna's model exhibits all the features of the Portevin - Le Chatelier effect including the three types of bands. The model reproduces the recently observed crossover from a low dimensional chaotic state at low and medium strain rates to a high dimensional power law state of stress drops at high strain rates. The dynamics of crossover is elucidated through a study of the Lyapunov spectrum.

Large latitudinal gradients and temporal heterogeneity in aerosol black carbon and its mass mixing ratio over southern and northern oceans observed during a trans-continental cruise experiment

Extensive, and collocated measurements of the mass concentrations (M-B) of aerosol black carbon (BC) and (M-T) of composite aerosols were made over the Arabian Sea, tropical Indian Ocean and the Southern Ocean during a trans-continental cruise experiment. Our investigations show that MB remains extremely low(<50 ng m(-3)) and remarkably steady (in space and time) in the Southern Ocean (20 degrees S to 56 degrees S). In contrast, large latitudinal gradients exist north of similar to 20 degrees S; M-B increasing exponentially to reach as high as 2000 ng m(-3) in the Arabian Sea (similar to 8 degrees N). Interestingly, the share of BC showed a distinctly different latitudinal variation, with a peak close to the equator and decreasing on either side. Large fluctuations were seen in M-T over Southern Ocean associated with enhanced production of sea-salt aerosols in response to sea-surface wind speed. These spatio-temporal changes in M-B and its mixing ratio have important implications to regional and global climate.

Temporal associations in fig-wasp-ant interactions: diel and phenological patterns

In a complex multitrophic plant-animal interaction system in which there are direct and indirect interactions between species, comprehending the dynamics of these multiple partners is very important for an understanding of how the system is structured. We investigated the plant Ficus racemosa L. (Moraceae) and its community of obligatory mutualistic and parasitic fig wasps (Hymenoptera: Chalcidoidea) that develop within the fig inflorescence or syconium, as well as their interaction with opportunistic ants. We focused on temporal resource partitioning among members of the fig wasp community over the development cycle of the fig syconia during which wasp oviposition and development occur and we studied the activity rhythm of the ants associated with this community. We found that the seven members of the wasp community partitioned their oviposition across fig syconium development phenology and showed interspecific variation in activity across the day-night cycle. The wasps presented a distinct sequence in their arrival at fig syconia for oviposition, with the parasitoid wasps following the galling wasps. Although fig wasps are known to be largely diurnal, we documented night oviposition in several fig wasp species for the first time. Ant activity on the fig syconia was correlated with wasp activity and was dependent on whether the ants were predatory or trophobiont-tending species; only numbers of predatory ants increased during peak arrivals of the wasps.

Vitellins and vitellogenins of Dysdercus koenigii (Heteroptera : Pyrrhocoridae) - identification, purification and temporal pattern

Two vitellins, VtA and VtB, were purified from the eggs of Dysdercus koenigii by gel filtration and ion exchange chromatography. VtA and VtB have molecular weights of 290 and 260 kDa, respectively. Both Vts are glycolipoproteinaceous in nature. VtA is composed of three polypeptides of M-r 116, 92 and 62 kDa while VtB contained an additional subunit of M-r 40 kDa. All subunits except the 116-kDa subunit are glycolipopolypeptides. Polyclonal antibody raised against VtA (anti-VtA antibody) cross-reacted with VtB and also with vitellogenic haemolymph and ovaries and pre-vitellogenic fat bodies, but not with haemolymph from either adult male, fifth instar female, or pre-vitellogenic females demonstrating sex and stage specificity of the Vts. Immunoblots in the presence of anti-VtA revealed two proteins (of 290 and 260 kDa) in both vitellogenic haemolymph and pre-vitellogenic fat bodies that are recognised as D. koenigii Vgs. In newly emerged females, Vgs appeared on day 1 in fat bodies and on day 3 in haemolymph and ovaries. Vg concentration was maximum on day 2 in fat body, day 4 in haemolymph and day 7 in ovary. Although the biochemical and temporal characteristics of these proteins show similarity to some hemipterans, they are strikingly dissimilar with those of a very closely related species. (C) 1999 Elsevier Science Inc. All rights reserved.

Conflict-Tolerant Real-Time Specifications in Metric Temporal Logic

A framework based on the notion of "conflict-tolerance" was proposed in as a compositional methodology for developing and reasoning about systems that comprise multiple independent controllers. A central notion in this framework is that of a "conflict-tolerant" specification for a controller. In this work we propose a way of defining conflict-tolerant real-time specifications in Metric Interval Temporal Logic (MITL). We call our logic CT-MITL for Conflict-Tolerant MITL. We then give a clock optimal "delay-then-extend" construction for building a timed transition system for monitoring past-MITL formulas. We show how this monitoring transition system can be used to solve the associated verification and synthesis problems for CT-MITL.